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
chore: changes to adapt to leanprover/lean4#2644 #7606
Conversation
Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean
Outdated
Show resolved
Hide resolved
@@ -34,7 +34,8 @@ def monoidalClosedHomEquiv (M N P : ModuleCat.{u} R) : | |||
left_inv f := by | |||
apply TensorProduct.ext' | |||
intro m n | |||
rw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply, | |||
-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 | |||
erw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply, |
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.
There is some strange behavior here. If I break out the terms that need erw
then the following closes the goal alone
erw [coe_comp]
rw [Function.comp_apply]
erw [MonoidalCategory.braiding_hom_apply, TensorProduct.lift.tmul]
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…y/mathlib4 into lean-pr-testing-2644
-- This lemma has always been bad, but lean4#2644 made `simp` start noticing | ||
@[simp, nolint simpNF] | ||
theorem ε_apply (r : R) : ε R r = Finsupp.single PUnit.unit r := |
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.
If ε
is an implementation detail, then presumably we can use local simp
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.
Feel free to make such changes yourself, but otherwise I'm going to leave these for "later".
namespace NameSet | ||
|
||
/-- The union of two `NameSet`s. -/ | ||
def append (s t : NameSet) : NameSet := | ||
s.mergeBy (fun _ _ _ => .unit) t | ||
|
||
instance : Append NameSet where | ||
append := NameSet.append | ||
|
||
end NameSet | ||
|
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.
You can ignore the changes to this file. They are needed here to get Mathlib to compile against this toolchain, but do not need to be reviewed.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Closing in favour of the actual bump PR, #7703 |
This includes all the changes from #7606. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover/lean4#2644