fix: fix simp lemmas about coercion to function (#2270)

Mathlib/Algebra/Group/WithOne/Basic.lean

@@ -108,7 +108,7 @@ def map (f : α →ₙ* β) : WithOne α →* WithOne β :=
 
 @[to_additive (attr := simp)]
 theorem map_coe (f : α →ₙ* β) (a : α) : map f (a : WithOne α) = f a :=
-  lift_coe _ _
+  rfl
 #align with_one.map_coe WithOne.map_coe
 #align with_zero.map_coe WithZero.map_coe
 
@@ -138,10 +138,8 @@ theorem map_comp (f : α →ₙ* β) (g : β →ₙ* γ) : map (g.comp f) = (map
 def _root_.MulEquiv.withOneCongr (e : α ≃* β) : WithOne α ≃* WithOne β :=
   { map e.toMulHom with
     toFun := map e.toMulHom, invFun := map e.symm.toMulHom,
-    left_inv := fun x => (map_map _ _ _).trans <| by
-      induction x using WithOne.cases_on <;> simp
-    right_inv := fun x => (map_map _ _ _).trans <| by
-      induction x using WithOne.cases_on <;> simp }
+    left_inv := (by induction · using WithOne.cases_on <;> simp)
+    right_inv := (by induction · using WithOne.cases_on <;> simp) }
 #align mul_equiv.with_one_congr MulEquiv.withOneCongr
 #align add_equiv.with_zero_congr AddEquiv.withZeroCongr
 

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -201,12 +201,16 @@ variable [Mul M] [Mul N] [Mul P] [Mul Q]
 -- Porting note: `to_fun_eq_coe` no longer needed in Lean4
 #noalign mul_equiv.to_fun_eq_coe
 #noalign add_equiv.to_fun_eq_coe
--- Porting note: `coe_to_equiv` no longer needed in Lean4
-#noalign mul_equiv.coe_to_equiv
-#noalign add_equiv.coe_to_equiv
 
 @[to_additive (attr := simp)]
-theorem coe_toMulHom {f : M ≃* N} : f.toMulHom = f.toFun := rfl
+theorem coe_toEquiv (f : M ≃* N) : (f.toEquiv : M → N) = f := rfl
+#align mul_equiv.coe_to_equiv MulEquiv.coe_toEquiv
+#align add_equiv.coe_to_equiv AddEquiv.coe_toEquiv
+
+-- porting note: todo: `MulHom.coe_mk` simplifies `↑f.toMulHom` to `f.toMulHom.toFun`,
+-- not `f.toEquiv.toFun`; use higher priority as a workaround
+@[to_additive (attr := simp 1100)]
+theorem coe_toMulHom {f : M ≃* N} : (f.toMulHom : M → N) = f := rfl
 #align mul_equiv.coe_to_mul_hom MulEquiv.coe_toMulHom
 #align add_equiv.coe_to_add_hom AddEquiv.coe_toAddHom
 
@@ -258,12 +262,18 @@ def symm {M N : Type _} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
 #align mul_equiv.symm MulEquiv.symm
 #align add_equiv.symm AddEquiv.symm
 
-@[to_additive (attr := simp)]
-theorem invFun_eq_symm {f : M ≃* N} : EquivLike.inv f = f.symm := rfl
+@[to_additive] -- porting note: no longer a `simp`, see below
+theorem invFun_eq_symm {f : M ≃* N} : f.invFun = f.symm := rfl
 #align mul_equiv.inv_fun_eq_symm MulEquiv.invFun_eq_symm
 -- Porting note: to_additive translated the name incorrectly in mathlib 3.
 #align add_equiv.neg_fun_eq_symm AddEquiv.invFun_eq_symm
 
+@[to_additive (attr := simp)]
+theorem coe_toEquiv_symm (f : M ≃* N) : (f.toEquiv.symm : N → M) = f.symm := rfl
+
+@[to_additive (attr := simp)]
+theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl
+
 -- we don't hyperlink the note in the additive version, since that breaks syntax highlighting
 -- in the whole file.
 
@@ -287,16 +297,18 @@ theorem toEquiv_symm (f : M ≃* N) : f.symm.toEquiv = f.toEquiv.symm := rfl
 #align mul_equiv.to_equiv_symm MulEquiv.toEquiv_symm
 #align add_equiv.to_equiv_symm AddEquiv.toEquiv_symm
 
--- Porting note: `coe_mk` no longer needed in Lean4
-#noalign mul_equiv.coe_mk
-#noalign add_equiv.coe_mk
+-- porting note: doesn't align with Mathlib 3 because `MulEquiv.mk` has a new signature
+@[to_additive (attr := simp)]
+theorem coe_mk (f : M ≃ N) (hf : ∀ x y, f (x * y) = f x * f y) : (mk f hf : M → N) = f := rfl
+#align mul_equiv.coe_mk MulEquiv.coe_mkₓ
+#align add_equiv.coe_mk AddEquiv.coe_mkₓ
+
 -- Porting note: `toEquiv_mk` no longer needed in Lean4
 #noalign mul_equiv.to_equiv_mk
 #noalign add_equiv.to_equiv_mk
 
 @[to_additive (attr := simp)]
-theorem symm_symm : ∀ f : M ≃* N, f.symm.symm = f
-  | ⟨_, _⟩ => rfl
+theorem symm_symm (f : M ≃* N) : f.symm.symm = f := rfl
 #align mul_equiv.symm_symm MulEquiv.symm_symm
 #align add_equiv.symm_symm AddEquiv.symm_symm
 
@@ -539,32 +551,24 @@ theorem map_ne_one_iff {M N} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x :
 #align mul_equiv.map_ne_one_iff MulEquiv.map_ne_one_iff
 #align add_equiv.map_ne_zero_iff AddEquiv.map_ne_zero_iff
 
--- porting note: Mathlib 3 had `@[simps apply]` but right now in Lean 4 it's generating
--- simp lemmas which don't lint.
 /-- A bijective `Semigroup` homomorphism is an isomorphism -/
-@[to_additive "A bijective `AddSemigroup` homomorphism is an isomorphism"]
+@[to_additive (attr := simps! apply) "A bijective `AddSemigroup` homomorphism is an isomorphism"]
 noncomputable def ofBijective {M N F} [Mul M] [Mul N] [MulHomClass F M N]
 (f : F) (hf : Function.Bijective f) :
     M ≃* N :=
   { Equiv.ofBijective f hf with map_mul' := map_mul f }
 #align mul_equiv.of_bijective MulEquiv.ofBijective
 #align add_equiv.of_bijective AddEquiv.ofBijective
-
--- porting note: `@[simps apply]` should be making this lemma but it actually makes
--- a lemma with `toFun` which isn't in simp normal form.
-@[to_additive (attr := simp)] theorem ofBijective_apply {M N F} [Mul M] [Mul N] [MulHomClass F M N]
-    (f : F) (hf : Function.Bijective f) (a : M) : (MulEquiv.ofBijective f hf).toEquiv a = f a :=
-  rfl
 #align mul_equiv.of_bijective_apply MulEquiv.ofBijective_apply
 #align add_equiv.of_bijective_apply AddEquiv.ofBijective_apply
 
+-- porting note: todo: simplify `symm_apply` to `surjInv`?
 @[to_additive (attr := simp)]
 theorem ofBijective_apply_symm_apply {M N} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N)
     (hf : Function.Bijective f) : f ((Equiv.ofBijective f hf).symm n) = n :=
   (MulEquiv.ofBijective f hf).apply_symm_apply n
 #align mul_equiv.of_bijective_apply_symm_apply MulEquiv.ofBijective_apply_symm_apply
--- Porting note: No to_additive version in mathlib 3
--- #align add_equiv.of_bijective_apply_symm_apply AddEquiv.ofBijective_apply_symm_apply
+#align add_equiv.of_bijective_apply_symm_apply AddEquiv.ofBijective_apply_symm_apply
 
 /-- Extract the forward direction of a multiplicative equivalence
 as a multiplication-preserving function.
@@ -578,7 +582,7 @@ def toMonoidHom {M N} [MulOneClass M] [MulOneClass N] (h : M ≃* N) : M →* N
 
 @[to_additive (attr := simp)]
 theorem coe_toMonoidHom {M N} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
-  ↑e.toMonoidHom = ⇑e := rfl
+  ⇑e.toMonoidHom = e := rfl
 #align mul_equiv.coe_to_monoid_hom MulEquiv.coe_toMonoidHom
 #align add_equiv.coe_to_add_monoid_hom AddEquiv.coe_toAddMonoidHom
 
@@ -610,7 +614,7 @@ def arrowCongr {M N P Q : Type _} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) :
 /-- A multiplicative analogue of `Equiv.arrowCongr`,
 for multiplicative maps from a monoid to a commutative monoid.
 -/
-@[to_additive
+@[to_additive (attr := simps apply)
   "An additive analogue of `Equiv.arrowCongr`,
   for additive maps from an additive monoid to a commutative additive monoid."]
 -- porting note: @[simps apply] removed because it was making a lemma which
@@ -625,12 +629,6 @@ def monoidHomCongr {M N P Q} [MulOneClass M] [MulOneClass N] [CommMonoid P] [Com
   map_mul' h k := by ext; simp
 #align mul_equiv.monoid_hom_congr MulEquiv.monoidHomCongr
 #align add_equiv.add_monoid_hom_congr AddEquiv.addMonoidHomCongr
-
-@[to_additive (attr := simp)] theorem monoidHomCongr_apply {M N P Q} [MulOneClass M] [MulOneClass N]
-    [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
-    (MulEquiv.monoidHomCongr f g).toEquiv h = MonoidHom.comp (MulEquiv.toMonoidHom g)
-    (MonoidHom.comp h (MulEquiv.toMonoidHom (MulEquiv.symm f))) :=
-  rfl
 #align mul_equiv.monoid_hom_congr_apply MulEquiv.monoidHomCongr_apply
 #align add_equiv.add_monoid_hom_congr_apply AddEquiv.addMonoidHomCongr_apply
 
@@ -678,30 +676,16 @@ theorem piCongrRight_trans {η : Type _} {Ms Ns Ps : η → Type _} [∀ j, Mul
 
 /-- A family indexed by a nonempty subsingleton type is equivalent to the element at the single
 index. -/
-@[to_additive
+@[to_additive (attr := simps!)
   "A family indexed by a nonempty subsingleton type is
   equivalent to the element at the single index."]
 def piSubsingleton {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)] [Subsingleton ι]
   (i : ι) : (∀ j, M j) ≃* M i :=
   { Equiv.piSubsingleton M i with map_mul' := fun _ _ => Pi.mul_apply _ _ _ }
 #align mul_equiv.Pi_subsingleton MulEquiv.piSubsingleton
 #align add_equiv.Pi_subsingleton AddEquiv.piSubsingleton
-
--- porting note: the next two lemmas should be being generated by `@[to_additive, simps]`.
--- They are added manually because `@[simps]` is currently generating lemmas with `toFun` in
-@[to_additive (attr := simp)]
-theorem piSubsingleton_apply {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)]
-    [Subsingleton ι] (i : ι) (f : (x : ι) → M x) : (MulEquiv.piSubsingleton M i).toEquiv f = f i :=
-  rfl
 #align mul_equiv.Pi_subsingleton_apply MulEquiv.piSubsingleton_apply
 #align add_equiv.Pi_subsingleton_apply AddEquiv.piSubsingleton_apply
-
-@[to_additive (attr := simp)]
-theorem piSubsingleton_symmApply {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)]
-    [Subsingleton ι] (i : ι) (x : M i) (b : ι) :
-    (MulEquiv.symm (MulEquiv.piSubsingleton M i)) x b =
-    cast (Subsingleton.elim i b ▸ rfl : M i = M b) x :=
-rfl
 #align mul_equiv.Pi_subsingleton_symm_apply MulEquiv.piSubsingleton_symmApply
 #align add_equiv.Pi_subsingleton_symm_apply AddEquiv.piSubsingleton_symmApply
 
@@ -755,7 +739,7 @@ def MulHom.toMulEquiv [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁
 @[to_additive (attr := simp)]
 theorem MulHom.toMulEquiv_apply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
     (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.id _) :
-    ((MulHom.toMulEquiv f g h₁ h₂).toEquiv : M → N) = f :=
+    ((MulHom.toMulEquiv f g h₁ h₂) : M → N) = f :=
   rfl
 #align mul_hom.to_mul_equiv_apply MulHom.toMulEquiv_apply
 #align add_hom.to_add_equiv_apply AddHom.toAddEquiv_apply
@@ -768,12 +752,10 @@ theorem MulHom.toMulEquiv_symmApply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →
 #align mul_hom.to_mul_equiv_symm_apply MulHom.toMulEquiv_symmApply
 #align add_hom.to_add_equiv_symm_apply AddHom.toAddEquiv_symmApply
 
--- porting note: `@[simps (config := { fullyApplied := false })]` generates a simp lemma
--- which is not in simp normal form, so we add them manually
 /-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
 returns an multiplicative equivalence with `toFun = f` and `invFun = g`.  This constructor is
 useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
-@[to_additive
+@[to_additive (attr := simps (config := { fullyApplied := false }))
   "Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id`
   and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`.  This
   constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
@@ -787,23 +769,8 @@ def MonoidHom.toMulEquiv [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N 
   map_mul' := f.map_mul
 #align monoid_hom.to_mul_equiv MonoidHom.toMulEquiv
 #align add_monoid_hom.to_add_equiv AddMonoidHom.toAddEquiv
-
--- porting note: the next 2 lemmas should be being generated by
--- `@[to_additive, simps (config := { fullyApplied := false })]`
--- but right now it's generating `simp` lemmas which aren't in `simp` normal form.
-@[to_additive (attr := simp)]
-theorem MonoidHom.toMulEquiv_apply [MulOneClass M] [MulOneClass N] (f : M →* N)
-    (g : N →* M) (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) :
-    ((MonoidHom.toMulEquiv f g h₁ h₂).toEquiv : M → N) = ↑f :=
-  rfl
 #align monoid_hom.to_mul_equiv_apply MonoidHom.toMulEquiv_apply
 #align add_monoid_hom.to_add_equiv_apply AddMonoidHom.toAddEquiv_apply
-
-@[to_additive (attr := simp)]
-theorem MonoidHom.toMulEquiv_symmApply [MulOneClass M] [MulOneClass N]
-    (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) :
-    (MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂) : N → M) = g :=
-  rfl
 #align monoid_hom.to_mul_equiv_symm_apply MonoidHom.toMulEquiv_symmApply
 #align add_monoid_hom.to_add_equiv_symm_apply AddMonoidHom.toAddEquiv_symmApply
 

Mathlib/Algebra/Hom/Group.lean

@@ -588,13 +588,6 @@ instance MonoidWithZeroHom.coeToZeroHom {_ : MulZeroOneClass M} {_ : MulZeroOneC
   Coe (M →*₀ N) (ZeroHom M N) := ⟨MonoidWithZeroHom.toZeroHom⟩
 #align monoid_with_zero_hom.has_coe_to_zero_hom MonoidWithZeroHom.coeToZeroHom
 
--- Porting note: several `coe_eq_xxx` lemmas removed due to new `coe` in Lean4
-
-attribute [coe] OneHom.toFun
-attribute [coe] ZeroHom.toFun
-attribute [coe] MulHom.toFun
-attribute [coe] AddHom.toFun
-
 -- these must come after the coe_toFun definitions
 initialize_simps_projections ZeroHom (toFun → apply)
 initialize_simps_projections AddHom (toFun → apply)
@@ -604,29 +597,32 @@ initialize_simps_projections MulHom (toFun → apply)
 initialize_simps_projections MonoidHom (toOneHom_toFun → apply, -toOneHom)
 initialize_simps_projections MonoidWithZeroHom (toZeroHom_toFun → apply, -toZeroHom)
 
--- Porting note: removed several `toFun_eq_coe` lemmas due to new Coe in Lean4
-
 @[to_additive (attr := simp)]
 theorem OneHom.coe_mk [One M] [One N] (f : M → N) (h1) : (OneHom.mk f h1 : M → N) = f := rfl
 #align one_hom.coe_mk OneHom.coe_mk
 #align zero_hom.coe_mk ZeroHom.coe_mk
 
+@[to_additive (attr := simp)]
+theorem OneHom.toFun_eq_coe [One M] [One N] (f : OneHom M N) : f.toFun = f := rfl
+#align one_hom.to_fun_eq_coe OneHom.toFun_eq_coe
+#align zero_hom.to_fun_eq_coe ZeroHom.toFun_eq_coe
+
 @[to_additive (attr := simp)]
 theorem MulHom.coe_mk [Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f := rfl
 #align mul_hom.coe_mk MulHom.coe_mk
 #align add_hom.coe_mk AddHom.coe_mk
 
+@[to_additive (attr := simp)]
+theorem MulHom.toFun_eq_coe [Mul M] [Mul N] (f : M →ₙ* N) : f.toFun = f := rfl
+#align mul_hom.to_fun_eq_coe MulHom.toFun_eq_coe
+#align add_hom.to_fun_eq_coe AddHom.toFun_eq_coe
+
 @[to_additive (attr := simp)]
 theorem MonoidHom.coe_mk [MulOneClass M] [MulOneClass N] (f hmul) :
   (MonoidHom.mk f hmul : M → N) = f := rfl
 #align monoid_hom.coe_mk MonoidHom.coe_mk
 #align add_monoid_hom.coe_mk AddMonoidHom.coe_mk
 
-@[simp]
-theorem MonoidWithZeroHom.coe_mk [MulZeroOneClass M] [MulZeroOneClass N] (f h1 hmul) :
-  (MonoidWithZeroHom.mk f h1 hmul : M → N) = (f : M → N) := rfl
-#align monoid_with_zero_hom.coe_mk MonoidWithZeroHom.coe_mk
-
 @[to_additive (attr := simp)]
 theorem MonoidHom.toOneHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
   (f.toOneHom : M → N) = f := rfl
@@ -639,12 +635,21 @@ theorem MonoidHom.toMulHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
 #align monoid_hom.to_mul_hom_coe MonoidHom.toMulHom_coe
 #align add_monoid_hom.to_add_hom_coe AddMonoidHom.toAddHom_coe
 
+@[to_additive]
+theorem MonoidHom.toFun_eq_coe [MulOneClass M] [MulOneClass N] (f : M →* N) : f.toFun = f := rfl
+#align monoid_hom.to_fun_eq_coe MonoidHom.toFun_eq_coe
+#align add_monoid_hom.to_fun_eq_coe AddMonoidHom.toFun_eq_coe
+
+@[simp]
+theorem MonoidWithZeroHom.coe_mk [MulZeroOneClass M] [MulZeroOneClass N] (f h1 hmul) :
+  (MonoidWithZeroHom.mk f h1 hmul : M → N) = (f : M → N) := rfl
+#align monoid_with_zero_hom.coe_mk MonoidWithZeroHom.coe_mk
+
 @[simp]
 theorem MonoidWithZeroHom.toZeroHom_coe [MulZeroOneClass M] [MulZeroOneClass N] (f : M →*₀ N) :
   (f.toZeroHom : M → N) = f := rfl
 #align monoid_with_zero_hom.to_zero_hom_coe MonoidWithZeroHom.toZeroHom_coe
 
-@[simp]
 theorem MonoidWithZeroHom.toMonoidHom_coe [MulZeroOneClass M] [MulZeroOneClass N] (f : M →*₀ N) :
   f.toMonoidHom.toFun = f := rfl
 #align monoid_with_zero_hom.to_monoid_hom_coe MonoidWithZeroHom.toMonoidHom_coe

Mathlib/Algebra/Hom/Ring.lean

@@ -155,9 +155,7 @@ theorem coe_mulHom_mk (f : α → β) (h₁ h₂ h₃) :
   rfl
 #align non_unital_ring_hom.coe_mul_hom_mk NonUnitalRingHom.coe_mulHom_mk
 
-@[simp]
-theorem coe_toAddMonoidHom (f : α →ₙ+* β) : ↑(f.toMulHom) = ↑f :=
-  rfl
+theorem coe_toAddMonoidHom (f : α →ₙ+* β) : ⇑f.toAddMonoidHom = f := rfl
 #align non_unital_ring_hom.coe_to_add_monoid_hom NonUnitalRingHom.coe_toAddMonoidHom
 
 @[simp]

Mathlib/Algebra/Module/Equiv.lean

@@ -228,9 +228,8 @@ theorem coe_toLinearMap : ⇑e.toLinearMap = e :=
   rfl
 #align linear_equiv.coe_to_linear_map LinearEquiv.coe_toLinearMap
 
-@[simp]
-theorem toFun_eq_coe : e.toFun = e :=
-  rfl
+-- porting note: no longer a `simp`
+theorem toFun_eq_coe : e.toFun = e := rfl
 #align linear_equiv.to_fun_eq_coe LinearEquiv.toFun_eq_coe
 
 section

Mathlib/Algebra/Module/LinearMap.lean

@@ -231,9 +231,11 @@ def toDistribMulActionHom (f : M →ₗ[R] M₂) : DistribMulActionHom R M M₂
 #align linear_map.to_distrib_mul_action_hom LinearMap.toDistribMulActionHom
 
 @[simp]
-theorem to_fun_eq_coe {f : M →ₛₗ[σ] M₃} : f.toFun = (f : M → M₃) :=
-  rfl
-#align linear_map.to_fun_eq_coe LinearMap.to_fun_eq_coe
+theorem coe_toAddHom (f : M →ₛₗ[σ] M₃) : ⇑f.toAddHom = f := rfl
+
+-- porting note: no longer a `simp`
+theorem toFun_eq_coe {f : M →ₛₗ[σ] M₃} : f.toFun = (f : M → M₃) := rfl
+#align linear_map.to_fun_eq_coe LinearMap.toFun_eq_coe
 
 @[ext]
 theorem ext {f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g :=

Mathlib/Data/Finsupp/ToDfinsupp.lean

@@ -258,14 +258,6 @@ def finsuppLequivDfinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M]
     map_add' := Finsupp.toDfinsupp_add }
 #align finsupp_lequiv_dfinsupp finsuppLequivDfinsupp
 
--- porting note: the following three were previously generated by `simps`
-@[simp]
-theorem finsuppLequivDfinsupp_apply_toAddHom_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]
-    [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
-    (↑(finsuppLequivDfinsupp (M := M) R).toLinearMap.toAddHom : (ι →₀ M) → _) =
-      Finsupp.toDfinsupp :=
-  rfl
-
 -- porting note: `simps` generated as ` ↑(finsuppLequivDfinsupp R).toLinearMap = Finsupp.toDfinsupp`
 @[simp]
 theorem finsuppLequivDfinsupp_apply_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]

Mathlib/LinearAlgebra/Basic.lean

@@ -1901,11 +1901,11 @@ def submoduleMap (p : Submodule R M) : p ≃ₛₗ[σ₁₂] ↥(p.map (e : M 
         subst hxy
         simp only [symm_apply_apply, Submodule.coe_mk, coe_coe, hx]⟩
     left_inv := fun x => by
-      simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.to_fun_eq_coe,
+      simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
         LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, SetLike.eta]
     right_inv := fun y => by
       apply SetCoe.ext
-      simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.to_fun_eq_coe,
+      simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
         LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] }
 #align linear_equiv.submodule_map LinearEquiv.submoduleMap