chore: remove Equiv.toFun_as_coe_apply (#7902)

This `simp` lemma was added during the port but tagged as probably unnecessary after fixing leanprover/lean4#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.

Author: PatrickMassot

Mathlib/Data/MvPolynomial/Equiv.lean

@@ -270,7 +270,7 @@ def sumAlgEquiv : MvPolynomial (Sum S₁ S₂) R ≃ₐ[R] MvPolynomial S₁ (Mv
       intro r
       have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) : _) := rfl
       have B : algebraMap R (MvPolynomial (Sum S₁ S₂) R) r = C r := rfl
-      simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe_apply,
+      simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe,
         Equiv.coe_fn_mk, B, sumToIter_C, A] }
 #align mv_polynomial.sum_alg_equiv MvPolynomial.sumAlgEquiv
 

Mathlib/Logic/Equiv/Defs.lean

@@ -185,12 +185,6 @@ instance : Trans Equiv Equiv Equiv where
 @[simp, mfld_simps] theorem toFun_as_coe (e : α ≃ β) : e.toFun = e := rfl
 #align equiv.to_fun_as_coe Equiv.toFun_as_coe
 
--- porting note: `simp` should prove this using `toFun_as_coe`, but it doesn't.
--- This might be a bug in `simp` -- see https://github.com/leanprover/lean4/issues/1937
--- If this issue is fixed then the simp linter probably will start complaining, and
--- this theorem can be deleted hopefully without breaking any `simp` proofs.
-@[simp] theorem toFun_as_coe_apply (e : α ≃ β) (x : α) : e.toFun x = e x := rfl
-
 @[simp, mfld_simps] theorem invFun_as_coe (e : α ≃ β) : e.invFun = e.symm := rfl
 #align equiv.inv_fun_as_coe Equiv.invFun_as_coe
 

Mathlib/Logic/Equiv/TransferInstance.lean

@@ -534,7 +534,7 @@ def linearEquiv (e : α ≃ β) [AddCommMonoid β] [Module R β] : by
     { Equiv.addEquiv e with
       map_smul' := fun r x => by
         apply e.symm.injective
-        simp only [toFun_as_coe_apply, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]
+        simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]
         exact Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl }
 #align equiv.linear_equiv Equiv.linearEquiv
 

Mathlib/Topology/Homeomorph.lean

@@ -592,7 +592,7 @@ end
 def piCongrLeft {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)]
     (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ₜ ∀ j, Y j where
   continuous_toFun := continuous_pi <| e.forall_congr_left.mp <| fun i ↦ by
-    simpa only [Equiv.toFun_as_coe_apply, Equiv.piCongrLeft_apply_apply] using continuous_apply i
+    simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using continuous_apply i
   continuous_invFun := Pi.continuous_precomp' e
   toEquiv := Equiv.piCongrLeft _ e
 

Mathlib/Topology/UniformSpace/Equiv.lean

@@ -349,7 +349,7 @@ theorem coe_punitProd : ⇑(punitProd α) = Prod.snd :=
 def piCongrLeft {ι ι' : Type*} {β : ι' → Type*} [∀ j, UniformSpace (β j)]
     (e : ι ≃ ι') : (∀ i, β (e i)) ≃ᵤ ∀ j, β j where
   uniformContinuous_toFun := uniformContinuous_pi.mpr <| e.forall_congr_left.mp <| fun i ↦ by
-    simpa only [Equiv.toFun_as_coe_apply, Equiv.piCongrLeft_apply_apply] using
+    simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using
       Pi.uniformContinuous_proj _ i
   uniformContinuous_invFun := Pi.uniformContinuous_precomp' _ e
   toEquiv := Equiv.piCongrLeft _ e