Comment by thom

Lemme give an example of the kind of thing I'm picturing and you can tell me where it goes wrong. Lean Web tells me the following is fine:

  import Mathlib

  abbrev Scalar := ℂ
  abbrev Real := Scalar

  theorem negative_one_has_a_real_square_root :
      ∃ x : Real, x * x = -1 := by
    exact ⟨Complex.I, Complex.I_mul_I⟩

But we know it's a lie. I hide those abbrevs in 100k lines of stuff that you haven't yet checked manually. I don't understand what could be stopping shenanigans like these, though I appreciate you trying to show me!