-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*): move to lean-3.11.0 #2632
Conversation
@@ -133,7 +133,7 @@ by simpa using @conj_inj z 0 | |||
|
|||
lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r := | |||
⟨λ h, ⟨z.re, ext rfl $ eq_zero_of_neg_eq (congr_arg im h)⟩, | |||
λ ⟨h, e⟩, e.symm ▸ rfl⟩ | |||
λ ⟨h, e⟩, by rw [e, conj_of_real]⟩ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why does the old proof fail here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I made this change and I have no idea...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For what it's worth, the error message was:
/mathlib/src/data/complex/basic.lean:136:18: error: "eliminator" elaborator type mismatch, term
rfl
has type
?m_2 = ?m_2
but is expected to have type
conj ↑h = ↑h
Additional information:
/mathlib/src/data/complex/basic.lean:136:18: context: the inferred motive for the eliminator-like application is
λ (_x : ℂ), conj _x = _x
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure why it worked before. It would need to prove (-0 : real) = 0
by rfl
, which shouldn't be possible if the reals are irreducible.
The code changes seem fine to merge to me. I think the PR comment commit message should contain some more info though. |
bors r+ |
Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Pull request successfully merged into master. Build succeeded: |
Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs