-
Notifications
You must be signed in to change notification settings - Fork 259
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: forward port leanprover-community/mathlib#18575 #2899
Conversation
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.
a few regressions
Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
@@ -469,14 +456,13 @@ theorem coe_mul (f g : P1 →ᵃ[k] P1) : ⇑(f * g) = f ∘ g := | |||
#align affine_map.coe_mul AffineMap.coe_mul | |||
|
|||
@[simp] | |||
theorem coe_one : ⇑(1 : P1 →ᵃ[k] P1) = id k P1 := |
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.
This was a mis-port
@@ -853,7 +831,7 @@ theorem homothety_apply_same (c : P1) (r : k) : homothety c r c = c := | |||
|
|||
theorem homothety_mul_apply (c : P1) (r₁ r₂ : k) (p : P1) : | |||
homothety c (r₁ * r₂) p = homothety c r₁ (homothety c r₂ p) := by | |||
simp [homothety_apply, mul_smul] | |||
simp only [homothety_apply, mul_smul, vadd_vsub] |
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.
This proof was ported without modification the first time, but for whatever reason needs more help after this re-port
-- porting note: `simp` needs a placeholder for the `β` argument to `Set.mem_vsub` | ||
simp only [Set.mem_vsub (β := _), Set.mem_image, |
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.
This is deeply weird
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.
maintainer merge |
1 similar comment
maintainer merge |
isn't it |
I don't want to merge my own PR without the eyes of another maintainer. I posted again to try and wake up the bot, but it seems to be having github API issues, which we're working on resolving) |
Thanks! bors merge |
This somewhat re-ports the file from scratch (by manually cleaning up the mathport output to remove all the meta comments), as lots of workarounds were added in #2570 to deal with coercion issues. All proof changes are restoring the mathport proofs, except for small modifications to use `simp [(foo)]` instead of `simp [foo]` or `simp` (where `foo` was already a `simp` lemma). leanprover-community/mathlib#18575
Pull request successfully merged into master. Build succeeded:
|
This ran into many of the problems that #2899 did, where `simp` would fail but `simp [(foo)]` or `simp [foo _]` would succeed. Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
This somewhat re-ports the file from scratch (by manually cleaning up the mathport output to remove all the meta comments), as lots of workarounds were added in #2570 to deal with coercion issues.
All proof changes are restoring the mathport proofs, except for small modifications to use
simp [(foo)]
instead ofsimp [foo]
orsimp
(wherefoo
was already asimp
lemma).leanprover-community/mathlib#18575