I think you're misreading Lean Web. Over on the right side with that you'll see:
`Real` has already been declared
for your `abbrev Real`, and you'll see
our
Application type mismatch: The argument
Complex.I
has type
ℂ
but is expected to have type
ℝ
in the application
Exists.intro Complex.I
for the first term in your `exact` brackets.
It means that it rejects the proof. I suspect it may have been because you came back to the page too long after opening it, at which point you'll see `Lean server has stopped.` and won't get any type checking at all on Lean Web until you refresh.
But if I understand the point you're trying to make, that if you did shadow the name Real to actually mean Complex, then it would check, then yeah you're correct. But that's still where you just have to understand the statement, not the proof. The statements are never the giant 500k LoC part.
In a fixed version of your example, that means
- it's on you to understand that the statement unpacks to `∃ x : ℂ, x * x = -1`
- it's on you to look at whether the proof checker allows the proof (and potentially with what axioms, depending on your level of care)
- it's not on you to understand the proof
for the first term in your `exact` brackets.
It means that it rejects the proof. I suspect it may have been because you came back to the page too long after opening it, at which point you'll see `Lean server has stopped.` and won't get any type checking at all on Lean Web until you refresh.
But if I understand the point you're trying to make, that if you did shadow the name Real to actually mean Complex, then it would check, then yeah you're correct. But that's still where you just have to understand the statement, not the proof. The statements are never the giant 500k LoC part.
In a fixed version of your example, that means
- it's on you to understand that the statement unpacks to `∃ x : ℂ, x * x = -1`
- it's on you to look at whether the proof checker allows the proof (and potentially with what axioms, depending on your level of care)
- it's not on you to understand the proof