fix: add back lemmas deleted during porting (#3035)

These lemmas are not tautologies, despite the assumption that they were.
We know this because otherwise CI would fail.

After adding these back, a few statements downstream need to change from statements about `toEquiv` to statements about `EquivLike.toEquiv`.

Mathlib/Algebra/Algebra/Equiv.lean

@@ -129,6 +129,11 @@ instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
 def Simps.apply (e : A₁ ≃ₐ[R] A₂) : A₁ → A₂ :=
   e
 
+-- Porting note: the default simps projection was `e.toEquiv`, it should be `EquivLike.toEquiv`
+/-- See Note [custom simps projection] -/
+def Simps.toEquiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ A₂ :=
+  e
+
 -- Porting note: `protected` used to be an attribute below
 @[simp]
 protected theorem coe_coe {F : Type _} [AlgEquivClass F R A₁ A₂] (f : F) :
@@ -175,9 +180,12 @@ theorem mk_coe (e : A₁ ≃ₐ[R] A₂) (e' h₁ h₂ h₃ h₄ h₅) :
 #align alg_equiv.mk_coe AlgEquiv.mk_coe
 
 -- Porting note: `toFun_eq_coe` no longer needed in Lean4
-#noalign algebra_equiv.to_fun_eq_coe
--- Porting note: `toEquiv_eq_coe` no longer needed in Lean4
-#noalign algebra_equiv.to_equiv_eq_coe
+#noalign alg_equiv.to_fun_eq_coe
+
+@[simp]
+theorem toEquiv_eq_coe : e.toEquiv = e :=
+  rfl
+#align alg_equiv.to_equiv_eq_coe AlgEquiv.toEquiv_eq_coe
 
 @[simp]
 theorem toRingEquiv_eq_coe : e.toRingEquiv = e :=
@@ -189,9 +197,9 @@ theorem coe_ringEquiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e :=
   rfl
 #align alg_equiv.coe_ring_equiv AlgEquiv.coe_ringEquiv
 
-theorem coe_ring_equiv' : (e.toRingEquiv : A₁ → A₂) = e :=
+theorem coe_ringEquiv' : (e.toRingEquiv : A₁ → A₂) = e :=
   rfl
-#align alg_equiv.coe_ring_equiv' AlgEquiv.coe_ring_equiv'
+#align alg_equiv.coe_ring_equiv' AlgEquiv.coe_ringEquiv'
 
 theorem coe_ringEquiv_injective : Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ ≃+* A₂) :=
   fun _ _ h => ext <| RingEquiv.congr_fun h
@@ -331,7 +339,7 @@ theorem coe_coe_symm_apply_coe_apply {F : Type _} [AlgEquivClass F R A₁ A₂]
 
 -- Porting note: `simp` normal form of `invFun_eq_symm`
 @[simp]
-theorem symm_toEquiv_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.toEquiv.symm = e.symm :=
+theorem symm_toEquiv_eq_symm {e : A₁ ≃ₐ[R] A₂} : (e : A₁ ≃ A₂).symm = e.symm :=
   rfl
 
 theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=

Mathlib/Algebra/Group/Opposite.lean

@@ -242,7 +242,7 @@ def opAddEquiv [Add α] : α ≃+ αᵐᵒᵖ :=
 #align mul_opposite.op_add_equiv_symm_apply MulOpposite.opAddEquiv_symm_apply
 
 @[simp]
-theorem opAddEquiv_toEquiv [Add α] : (opAddEquiv : α ≃+ αᵐᵒᵖ).toEquiv = opEquiv := rfl
+theorem opAddEquiv_toEquiv [Add α] : ((opAddEquiv : α ≃+ αᵐᵒᵖ) : α ≃ αᵐᵒᵖ) = opEquiv := rfl
 
 #align mul_opposite.op_add_equiv_to_equiv MulOpposite.opAddEquiv_toEquiv
 
@@ -310,7 +310,7 @@ def opMulEquiv [Mul α] : α ≃* αᵃᵒᵖ :=
 #align add_opposite.op_mul_equiv_symm_apply AddOpposite.opMulEquiv_symm_apply
 
 @[simp]
-theorem opMulEquiv_toEquiv [Mul α] : (opMulEquiv : α ≃* αᵃᵒᵖ).toEquiv = opEquiv :=
+theorem opMulEquiv_toEquiv [Mul α] : ((opMulEquiv : α ≃* αᵃᵒᵖ) : α ≃ αᵃᵒᵖ) = opEquiv :=
   rfl
 #align add_opposite.op_mul_equiv_to_equiv AddOpposite.opMulEquiv_toEquiv
 

Mathlib/Algebra/Group/WithOne/Basic.lean

@@ -134,26 +134,15 @@ theorem map_comp (f : α →ₙ* β) (g : β →ₙ* γ) : map (g.comp f) = (map
 -- porting note: this used to have `@[simps apply]` but it was generating lemmas which
 -- weren't in simp normal form.
 /-- A version of `Equiv.optionCongr` for `WithOne`. -/
-@[to_additive "A version of `Equiv.optionCongr` for `WithZero`."]
+@[to_additive (attr := simps apply) "A version of `Equiv.optionCongr` for `WithZero`."]
 def _root_.MulEquiv.withOneCongr (e : α ≃* β) : WithOne α ≃* WithOne β :=
   { map e.toMulHom with
     toFun := map e.toMulHom, invFun := map e.symm.toMulHom,
     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
-
--- porting note: an approximation to this was being generated by `@[simps apply]` but it
--- mentioned Equiv.toFun so was not in simp normal form. This might be a bug in `@[simps].
-@[simp] theorem _root_.MulEquiv.withOneCongr_apply {α β : Type _} [Mul α] [Mul β] (e : α ≃* β)
-  (a : WithOne α) : (MulEquiv.withOneCongr e).toEquiv a = (map (MulEquiv.toMulHom e)) a := rfl
 #align mul_equiv.with_one_congr_apply MulEquiv.withOneCongr_apply
-
--- porting note: `@[to_additive, simps apply]` was not generating this lemma at the
--- time of writing this note.
-@[simp] theorem _root_.AddEquiv.withZeroCongr_apply {α β : Type _} [Add α] [Add β] (e : α ≃+ β)
-  (a : WithZero α) :
-    (AddEquiv.withZeroCongr e).toEquiv a = (WithZero.map (AddEquiv.toAddHom e)) a := rfl
 #align add_equiv.with_zero_congr_apply AddEquiv.withZeroCongr_apply
 
 -- porting note: for this declaration and the two below I added the `to_additive` attribute because

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -195,15 +195,18 @@ instance [Mul M] [Mul N] : MulEquivClass (M ≃* N) M N where
 
 variable [Mul M] [Mul N] [Mul P] [Mul Q]
 
--- Porting note: `to_equiv_eq_coe` no longer needed in Lean4
-#noalign mul_equiv.to_equiv_eq_coe
-#noalign add_equiv.to_equiv_eq_coe
+@[to_additive (attr := simp)]
+theorem toEquiv_eq_coe (f : M ≃* N) : f.toEquiv = f :=
+  rfl
+#align mul_equiv.to_equiv_eq_coe MulEquiv.toEquiv_eq_coe
+#align add_equiv.to_equiv_eq_coe AddEquiv.toEquiv_eq_coe
+
 -- 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
 
 @[to_additive (attr := simp)]
-theorem coe_toEquiv (f : M ≃* N) : (f.toEquiv : M → N) = f := rfl
+theorem coe_toEquiv (f : M ≃* N) : ⇑(f : M ≃ N) = f := rfl
 #align mul_equiv.coe_to_equiv MulEquiv.coe_toEquiv
 #align add_equiv.coe_to_equiv AddEquiv.coe_toEquiv
 
@@ -269,7 +272,7 @@ theorem invFun_eq_symm {f : M ≃* N} : f.invFun = f.symm := rfl
 #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
+theorem coe_toEquiv_symm (f : M ≃* N) : ((f : M ≃ N).symm : N → M) = f.symm := rfl
 
 @[to_additive (attr := simp)]
 theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl
@@ -278,7 +281,7 @@ theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl
 -- in the whole file.
 
 /-- See Note [custom simps projection] -/
-@[to_additive "See Note custom simps projection"]
+@[to_additive "See Note [custom simps projection]"] -- this comment fixes the syntax highlighting "
 def Simps.symm_apply (e : M ≃* N) : N → M :=
   e.symm
 #align mul_equiv.simps.symm_apply MulEquiv.Simps.symm_apply
@@ -289,7 +292,7 @@ initialize_simps_projections AddEquiv (toFun → apply, invFun → symm_apply)
 initialize_simps_projections MulEquiv (toFun → apply, invFun → symm_apply)
 
 @[to_additive (attr := simp)]
-theorem toEquiv_symm (f : M ≃* N) : f.symm.toEquiv = f.toEquiv.symm := rfl
+theorem toEquiv_symm (f : M ≃* N) : (f.symm : N ≃ M) = (f : M ≃ N).symm := rfl
 #align mul_equiv.to_equiv_symm MulEquiv.toEquiv_symm
 #align add_equiv.to_equiv_symm AddEquiv.toEquiv_symm
 

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

@@ -236,18 +236,12 @@ end Equiv
 -- aren't in simp normal form (they contain a `toFun`)
 /-- In a `DivisionCommMonoid`, `Equiv.inv` is a `MulEquiv`. There is a variant of this
 `MulEquiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case. -/
-@[to_additive "When the `AddGroup` is commutative, `Equiv.neg` is an `AddEquiv`."]
+@[to_additive (attr := simps apply)
+  "When the `AddGroup` is commutative, `Equiv.neg` is an `AddEquiv`."]
 def MulEquiv.inv (G : Type _) [DivisionCommMonoid G] : G ≃* G :=
   { Equiv.inv G with toFun := Inv.inv, invFun := Inv.inv, map_mul' := mul_inv }
 #align mul_equiv.inv MulEquiv.inv
 #align add_equiv.neg AddEquiv.neg
-
--- porting note: this lemma and the next are added manually because `simps` was
--- not quite generating the right thing
-@[to_additive (attr := simp)]
-theorem MulEquiv.inv_apply (G : Type _) [DivisionCommMonoid G] (a : G) :
-    (MulEquiv.inv G).toEquiv a = a⁻¹ :=
-  rfl
 #align mul_equiv.inv_apply MulEquiv.inv_apply
 #align add_equiv.neg_apply AddEquiv.neg_apply
 

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -1073,7 +1073,8 @@ protected noncomputable def opRingEquiv [Monoid G] :
   { opAddEquiv.symm.trans <|
       (Finsupp.mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ)).trans <| Finsupp.domCongr opEquiv with
     map_mul' := by
-      rw [Equiv.toFun_as_coe, AddEquiv.coe_toEquiv, ← AddEquiv.coe_toAddMonoidHom]
+      rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.coe_toEquiv,
+        ← AddEquiv.coe_toAddMonoidHom]
       refine Iff.mpr (AddMonoidHom.map_mul_iff (R := (MonoidAlgebra k G)ᵐᵒᵖ)
         (S := MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ) _) ?_
       -- Porting note: Was `ext`.
@@ -1816,7 +1817,8 @@ protected noncomputable def opRingEquiv [AddCommMonoid G] :
   { MulOpposite.opAddEquiv.symm.trans
       (Finsupp.mapRange.addEquiv (MulOpposite.opAddEquiv : k ≃+ kᵐᵒᵖ)) with
     map_mul' := by
-      rw [Equiv.toFun_as_coe, AddEquiv.coe_toEquiv, ← AddEquiv.coe_toAddMonoidHom]
+      rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.coe_toEquiv,
+        ← AddEquiv.coe_toAddMonoidHom]
       refine Iff.mpr (AddMonoidHom.map_mul_iff (R := (AddMonoidAlgebra k G)ᵐᵒᵖ)
         (S := AddMonoidAlgebra kᵐᵒᵖ G) _) ?_
       -- Porting note: Was `ext`.

Mathlib/Algebra/Ring/Equiv.lean

@@ -132,8 +132,11 @@ instance : RingEquivClass (R ≃+* S) R S where
   left_inv f := f.left_inv
   right_inv f := f.right_inv
 
--- Porting note: `toEquiv_eq_coe` no longer needed in Lean4
-#noalign ring_equiv.to_equiv_eq_coe
+@[simp]
+theorem toEquiv_eq_coe (f : R ≃+* S) : f.toEquiv = f :=
+  rfl
+#align ring_equiv.to_equiv_eq_coe RingEquiv.toEquiv_eq_coe
+
 -- Porting note: `toFun_eq_coe` no longer needed in Lean4
 #noalign ring_equiv.to_fun_eq_coe
 

Mathlib/Data/Finsupp/Basic.lean

@@ -286,8 +286,8 @@ theorem mapRange.addEquiv_toAddMonoidHom (f : M ≃+ N) :
 
 @[simp]
 theorem mapRange.addEquiv_toEquiv (f : M ≃+ N) :
-    (mapRange.addEquiv f).toEquiv =
-      (mapRange.equiv f.toEquiv f.map_zero f.symm.map_zero : (α →₀ _) ≃ _) :=
+    ↑(mapRange.addEquiv f : (α →₀ _) ≃+ _) =
+      (mapRange.equiv (f : M ≃ N) f.map_zero f.symm.map_zero : (α →₀ _) ≃ _) :=
   Equiv.ext fun _ => rfl
 #align finsupp.map_range.add_equiv_to_equiv Finsupp.mapRange.addEquiv_toEquiv
 

Mathlib/LinearAlgebra/Finsupp.lean

@@ -905,8 +905,8 @@ def sumFinsuppLEquivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R
       intros
       ext <;>
         -- Porting note: `add_equiv.to_fun_eq_coe` →
-        --               `Equiv.toFun_as_coe` & `AddEquiv.coe_toEquiv`
-        simp only [Equiv.toFun_as_coe, AddEquiv.coe_toEquiv, Prod.smul_fst,
+        --               `Equiv.toFun_as_coe` & `AddEquiv.toEquiv_eq_coe` & `AddEquiv.coe_toEquiv`
+        simp only [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.coe_toEquiv, Prod.smul_fst,
           Prod.smul_snd, smul_apply,
           snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp,
           RingHom.id_apply] }