[Merged by Bors] - fix(Mathlib/Algebra/Lie/DirectSum): remove unused R argument from lemmas#8388
[Merged by Bors] - fix(Mathlib/Algebra/Lie/DirectSum): remove unused R argument from lemmas#8388eric-wieser wants to merge 5 commits intomasterfrom
R argument from lemmas#8388Conversation
…emmas This made them not actually work as a `simp` lemma
ocfnash
left a comment
There was a problem hiding this comment.
Thanks for doing this. I'm surprised this wasn't caught by a linter (variable used in proof, not used in statement).
bors d+
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
I ended up with a small bit of scope creep when responding to review comments; mind taking another look @ocfnash? |
|
Looks great, thanks! bors merge |
|
👎 Rejected by label |
|
bors is just being very conservative (it's passed everything except for lean4checker) bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
…emmas (#8388) This made them not actually work as a `simp` lemma. Also extracts a common result that can be used to prove `single_add` for `DFinsupp` and `Finsupp`, and a new `Finsupp.single_mul` lemma.
|
Pull request successfully merged into master. Build succeeded: |
R argument from lemmasR argument from lemmas
What linter could possibly catch this? Certainly statements could require additional structure to hold, for example |
|
The simp linter should have caught that the simp lemma can't actually be proved with simp (and after #7905 it does) |
|
You are both absolutely right, thanks @eric-wieser and @alreadydone ! |
…emmas (#8388) This made them not actually work as a `simp` lemma. Also extracts a common result that can be used to prove `single_add` for `DFinsupp` and `Finsupp`, and a new `Finsupp.single_mul` lemma.
…emmas (#8388) This made them not actually work as a `simp` lemma. Also extracts a common result that can be used to prove `single_add` for `DFinsupp` and `Finsupp`, and a new `Finsupp.single_mul` lemma.
…emmas (#8388) This made them not actually work as a `simp` lemma. Also extracts a common result that can be used to prove `single_add` for `DFinsupp` and `Finsupp`, and a new `Finsupp.single_mul` lemma.
…20592) Uses the [`lie_of_same`](https://github.com/leanprover-community/mathlib4/blob/d4891b46ecc82d3f6050dd51c2699fee91a2347b/Mathlib/Algebra/Lie/DirectSum.lean#L118) lemma added in #8388 to shorten a 13-line proof down to a single line, removing two `erw`s and one porting note. According to `set_option trace.profiler true`, the new `lieAlgbraOf` declaration takes 135 milliseconds to elaborate, compared to 298 milliseconds for the declaration it replaces. Found via [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep).
…20592) Uses the [`lie_of_same`](https://github.com/leanprover-community/mathlib4/blob/d4891b46ecc82d3f6050dd51c2699fee91a2347b/Mathlib/Algebra/Lie/DirectSum.lean#L118) lemma added in #8388 to shorten a 13-line proof down to a single line, removing two `erw`s and one porting note. According to `set_option trace.profiler true`, the new `lieAlgbraOf` declaration takes 135 milliseconds to elaborate, compared to 298 milliseconds for the declaration it replaces. Found via [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep).
This made them not actually work as a
simplemma.Also extracts a common result that can be used to prove
single_addforDFinsuppandFinsupp, and a newFinsupp.single_mullemma.