Commit 2023-10-24 20:48 270b0eab

View on Github →

chore: remove Equiv.toFun_as_coe_apply (#7902) This simp lemma was added during the port but tagged as probably unnecessary after fixing https://github.com/leanprover/lean4/issues/1937. This PR confirms it is indeed no longer necessary. The only proofs that needed fixing were the one explicitly calling the new simp lemma. The porting note can go too.

Estimated changes

Modified Mathlib/Data/MvPolynomial/Equiv.lean

Modified Mathlib/Logic/Equiv/Defs.lean

deleted theorem Equiv.toFun_as_coe_apply

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/UniformSpace/Equiv.lean