Commit 2022-12-20 05:52 a2d69bdf

View on Github →

fix: reintroduce to_fun_as_coe as simp lemma (#931) This is a proposed fix for the broken simp calls in #922. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20calls.20broken.20in.20mathlib4.23922/near/314783451 for more details. Note that to_fun_as_coe was a syntactic tautology when it was ported, but this is no longer the case because we now have FunLike.

Estimated changes

Modified Mathlib/Algebra/Group/WithOne/Basic.lean

added theorem AddEquiv.withZeroCongr_apply

added theorem MulEquiv.withOneCongr_apply

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

added theorem MonoidHom.toMulEquiv_apply

added theorem MonoidHom.toMulEquiv_symmApply

added theorem MulEquiv.monoidHomCongr_apply

added theorem MulEquiv.ofBijective_apply

added theorem MulEquiv.piSubsingleton_apply

added theorem MulEquiv.piSubsingleton_symmApply

added theorem MulHom.toMulEquiv_apply

added theorem MulHom.toMulEquiv_symmApply

Modified Mathlib/Algebra/Hom/Equiv/Units/Basic.lean

added theorem AddEquiv.neg_apply

added theorem MulEquiv.inv_apply

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem Equiv.to_fun_as_coe

added theorem Equiv.to_fun_as_coe_apply

Modified Mathlib/Order/RelIso/Group.lean

added theorem RelIso.coe_mul

added theorem RelIso.coe_one

deleted theorem RelIso.toFun_mul

deleted theorem RelIso.toFun_one