fix: replace symmApply by symm_apply (#2560)

Author: fpvandoorn

Mathlib/Algebra/Algebra/Equiv.lean

@@ -311,11 +311,11 @@ def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
 #align alg_equiv.symm AlgEquiv.symm
 
 /-- See Note [custom simps projection] -/
-def Simps.symmApply (e : A₁ ≃ₐ[R] A₂) : A₂ → A₁ :=
+def Simps.symm_apply (e : A₁ ≃ₐ[R] A₂) : A₂ → A₁ :=
   e.symm
-#align alg_equiv.simps.symm_apply AlgEquiv.Simps.symmApply
+#align alg_equiv.simps.symm_apply AlgEquiv.Simps.symm_apply
 
-initialize_simps_projections AlgEquiv (toEquiv_toFun → apply,toEquiv_invFun → symmApply)
+initialize_simps_projections AlgEquiv (toEquiv_toFun → apply,toEquiv_invFun → symm_apply)
 
 --@[simp] -- Porting note: simp can prove this once symm_mk is introduced
 theorem coe_apply_coe_coe_symm_apply {F : Type _} [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) :
@@ -631,7 +631,7 @@ end OfLinearEquiv
 section OfRingEquiv
 
 /-- Promotes a linear ring_equiv to an AlgEquiv. -/
-@[simps apply symmApply toEquiv] -- Porting note: don't want redundant `toEquiv_symm_apply` simps
+@[simps apply symm_apply toEquiv] -- Porting note: don't want redundant `toEquiv_symm_apply` simps
 def ofRingEquiv {f : A₁ ≃+* A₂} (hf : ∀ x, f (algebraMap R A₁ x) = algebraMap R A₂ x) :
     A₁ ≃ₐ[R] A₂ :=
   { f with
@@ -794,7 +794,7 @@ variable [Group G] [MulSemiringAction G A] [SMulCommClass G R A]
 
 This is a stronger version of `MulSemiringAction.toRingEquiv` and
 `DistribMulAction.toLinearEquiv`. -/
-@[simps! apply symmApply toEquiv] -- Porting note: don't want redundant simps lemma `toEquiv_symm`
+@[simps! apply symm_apply toEquiv] -- Porting note: don't want redundant simps lemma `toEquiv_symm`
 def toAlgEquiv (g : G) : A ≃ₐ[R] A :=
   { MulSemiringAction.toRingEquiv _ _ g, MulSemiringAction.toAlgHom R A g with }
 #align mul_semiring_action.to_alg_equiv MulSemiringAction.toAlgEquiv

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -970,7 +970,7 @@ def associatesEquivOfUniqueUnits : Associates α ≃* α where
   right_inv _ := (Associates.out_mk _).trans <| normalize_eq _
   map_mul' := Associates.out_mul
 #align associates_equiv_of_unique_units associatesEquivOfUniqueUnits
-#align associates_equiv_of_unique_units_symm_apply associatesEquivOfUniqueUnits_symmApply
+#align associates_equiv_of_unique_units_symm_apply associatesEquivOfUniqueUnits_symm_apply
 #align associates_equiv_of_unique_units_apply associatesEquivOfUniqueUnits_apply
 
 end UniqueUnit

Mathlib/Algebra/Group/Opposite.lean

@@ -238,7 +238,7 @@ attribute [nolint simpComm] AddOpposite.commute_unop
 def opAddEquiv [Add α] : α ≃+ αᵐᵒᵖ :=
   { opEquiv with map_add' := fun _ _ => rfl }
 #align mul_opposite.op_add_equiv MulOpposite.opAddEquiv
-#align mul_opposite.op_add_equiv_symm_apply MulOpposite.opAddEquiv_symmApply
+#align mul_opposite.op_add_equiv_symm_apply MulOpposite.opAddEquiv_symm_apply
 
 @[simp]
 theorem opAddEquiv_toEquiv [Add α] : (opAddEquiv : α ≃+ αᵐᵒᵖ).toEquiv = opEquiv := rfl
@@ -306,7 +306,7 @@ variable {α}
 def opMulEquiv [Mul α] : α ≃* αᵃᵒᵖ :=
   { opEquiv with map_mul' := fun _ _ => rfl }
 #align add_opposite.op_mul_equiv AddOpposite.opMulEquiv
-#align add_opposite.op_mul_equiv_symm_apply AddOpposite.opMulEquiv_symmApply
+#align add_opposite.op_mul_equiv_symm_apply AddOpposite.opMulEquiv_symm_apply
 
 @[simp]
 theorem opMulEquiv_toEquiv [Mul α] : (opMulEquiv : α ≃* αᵃᵒᵖ).toEquiv = opEquiv :=
@@ -326,8 +326,8 @@ def MulEquiv.inv' (G : Type _) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ :=
   { (Equiv.inv G).trans opEquiv with map_mul' := fun x y => unop_injective <| mul_inv_rev x y }
 #align mul_equiv.inv' MulEquiv.inv'
 #align add_equiv.neg' AddEquiv.neg'
-#align mul_equiv.inv'_symm_apply MulEquiv.inv'_symmApply
-#align add_equiv.inv'_symm_apply AddEquiv.neg'_symmApply
+#align mul_equiv.inv'_symm_apply MulEquiv.inv'_symm_apply
+#align add_equiv.inv'_symm_apply AddEquiv.neg'_symm_apply
 
 /-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
 defines a semigroup homomorphism to `Nᵐᵒᵖ`. -/
@@ -560,13 +560,13 @@ def MulEquiv.op {α β} [Mul α] [Mul β] : α ≃* β ≃ (αᵐᵒᵖ ≃* β
   right_inv _ := rfl
 #align mul_equiv.op MulEquiv.op
 #align add_equiv.op AddEquiv.op
-#align mul_equiv.op_symm_apply_symm_apply MulEquiv.op_symm_apply_symmApply
+#align mul_equiv.op_symm_apply_symm_apply MulEquiv.op_symm_apply_symm_apply
 #align mul_equiv.op_apply_apply MulEquiv.op_apply_apply
-#align mul_equiv.op_apply_symm_apply MulEquiv.op_apply_symmApply
+#align mul_equiv.op_apply_symm_apply MulEquiv.op_apply_symm_apply
 #align mul_equiv.op_symm_apply_apply MulEquiv.op_symm_apply_apply
-#align add_equiv.op_symm_apply_symm_apply AddEquiv.op_symm_apply_symmApply
+#align add_equiv.op_symm_apply_symm_apply AddEquiv.op_symm_apply_symm_apply
 #align add_equiv.op_apply_apply AddEquiv.op_apply_apply
-#align add_equiv.op_apply_symm_apply AddEquiv.op_apply_symmApply
+#align add_equiv.op_apply_symm_apply AddEquiv.op_apply_symm_apply
 #align add_equiv.op_symm_apply_apply AddEquiv.op_symm_apply_apply
 
 /-- The 'unopposite' of an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. Inverse to `MulEquiv.op`. -/

Mathlib/Algebra/GroupRingAction/Basic.lean

@@ -74,7 +74,7 @@ theorem toRingHom_injective [MulSemiringAction M R] [FaithfulSMul M R] :
 def MulSemiringAction.toRingEquiv [MulSemiringAction G R] (x : G) : R ≃+* R :=
   { DistribMulAction.toAddEquiv R x, MulSemiringAction.toRingHom G R x with }
 #align mul_semiring_action.to_ring_equiv MulSemiringAction.toRingEquiv
-#align mul_semiring_action.to_ring_equiv_symm_apply MulSemiringAction.toRingEquiv_symmApply
+#align mul_semiring_action.to_ring_equiv_symm_apply MulSemiringAction.toRingEquiv_symm_apply
 #align mul_semiring_action.to_ring_equiv_apply MulSemiringAction.toRingEquiv_apply
 
 section

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -283,14 +283,14 @@ theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl
 def Simps.apply (e : M ≃* N) : M → N := e
 /-- See Note [custom simps projection] -/
 @[to_additive "See Note custom simps projection"]
-def Simps.symmApply (e : M ≃* N) : N → M :=
+def Simps.symm_apply (e : M ≃* N) : N → M :=
   e.symm
-#align mul_equiv.simps.symm_apply MulEquiv.Simps.symmApply
-#align add_equiv.simps.symm_apply AddEquiv.Simps.symmApply
+#align mul_equiv.simps.symm_apply MulEquiv.Simps.symm_apply
+#align add_equiv.simps.symm_apply AddEquiv.Simps.symm_apply
 
-initialize_simps_projections AddEquiv (toFun → apply, invFun → symmApply)
+initialize_simps_projections AddEquiv (toFun → apply, invFun → symm_apply)
 
-initialize_simps_projections MulEquiv (toFun → apply, invFun → symmApply)
+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
@@ -686,8 +686,8 @@ def piSubsingleton {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)] [Subsing
 #align add_equiv.Pi_subsingleton AddEquiv.piSubsingleton
 #align mul_equiv.Pi_subsingleton_apply MulEquiv.piSubsingleton_apply
 #align add_equiv.Pi_subsingleton_apply AddEquiv.piSubsingleton_apply
-#align mul_equiv.Pi_subsingleton_symm_apply MulEquiv.piSubsingleton_symmApply
-#align add_equiv.Pi_subsingleton_symm_apply AddEquiv.piSubsingleton_symmApply
+#align mul_equiv.Pi_subsingleton_symm_apply MulEquiv.piSubsingleton_symm_apply
+#align add_equiv.Pi_subsingleton_symm_apply AddEquiv.piSubsingleton_symm_apply
 
 /-!
 # Groups
@@ -745,12 +745,12 @@ theorem MulHom.toMulEquiv_apply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ*
 #align add_hom.to_add_equiv_apply AddHom.toAddEquiv_apply
 
 @[to_additive (attr := simp)]
-theorem MulHom.toMulEquiv_symmApply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
+theorem MulHom.toMulEquiv_symm_apply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
     (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.id _) :
     (MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂) : N → M) = ↑g :=
   rfl
-#align mul_hom.to_mul_equiv_symm_apply MulHom.toMulEquiv_symmApply
-#align add_hom.to_add_equiv_symm_apply AddHom.toAddEquiv_symmApply
+#align mul_hom.to_mul_equiv_symm_apply MulHom.toMulEquiv_symm_apply
+#align add_hom.to_add_equiv_symm_apply AddHom.toAddEquiv_symm_apply
 
 /-- 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
@@ -771,8 +771,8 @@ def MonoidHom.toMulEquiv [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N 
 #align add_monoid_hom.to_add_equiv AddMonoidHom.toAddEquiv
 #align monoid_hom.to_mul_equiv_apply MonoidHom.toMulEquiv_apply
 #align add_monoid_hom.to_add_equiv_apply AddMonoidHom.toAddEquiv_apply
-#align monoid_hom.to_mul_equiv_symm_apply MonoidHom.toMulEquiv_symmApply
-#align add_monoid_hom.to_add_equiv_symm_apply AddMonoidHom.toAddEquiv_symmApply
+#align monoid_hom.to_mul_equiv_symm_apply MonoidHom.toMulEquiv_symm_apply
+#align add_monoid_hom.to_add_equiv_symm_apply AddMonoidHom.toAddEquiv_symm_apply
 
 namespace Equiv
 

Mathlib/Algebra/Module/Equiv.lean

@@ -290,14 +290,14 @@ def Simps.apply {R : Type _} {S : Type _} [Semiring R] [Semiring S]
 #align linear_equiv.simps.apply LinearEquiv.Simps.apply
 
 /-- See Note [custom simps projection] -/
-def Simps.symmApply {R : Type _} {S : Type _} [Semiring R] [Semiring S]
+def Simps.symm_apply {R : Type _} {S : Type _} [Semiring R] [Semiring S]
     {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
     {M : Type _} {M₂ : Type _} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
     (e : M ≃ₛₗ[σ] M₂) : M₂ → M :=
   e.symm
-#align linear_equiv.simps.symm_apply LinearEquiv.Simps.symmApply
+#align linear_equiv.simps.symm_apply LinearEquiv.Simps.symm_apply
 
-initialize_simps_projections LinearEquiv (toFun → apply, invFun → symmApply)
+initialize_simps_projections LinearEquiv (toFun → apply, invFun → symm_apply)
 
 @[simp]
 theorem invFun_eq_symm : e.invFun = e.symm :=
@@ -586,7 +586,7 @@ def _root_.RingEquiv.toSemilinearEquiv (f : R ≃+* S) :
     toFun := f
     map_smul' := f.map_mul }
 #align ring_equiv.to_semilinear_equiv RingEquiv.toSemilinearEquiv
-#align ring_equiv.to_semilinear_equiv_symm_apply RingEquiv.toSemilinearEquiv_symmApply
+#align ring_equiv.to_semilinear_equiv_symm_apply RingEquiv.toSemilinearEquiv_symm_apply
 
 variable [Semiring R₁] [Semiring R₂] [Semiring R₃]
 
@@ -624,7 +624,7 @@ def restrictScalars (f : M ≃ₗ[S] M₂) : M ≃ₗ[R] M₂ :=
     right_inv := f.right_inv }
 #align linear_equiv.restrict_scalars LinearEquiv.restrictScalars
 #align linear_equiv.restrict_scalars_apply LinearEquiv.restrictScalars_apply
-#align linear_equiv.restrict_scalars_symm_apply LinearEquiv.restrictScalars_symmApply
+#align linear_equiv.restrict_scalars_symm_apply LinearEquiv.restrictScalars_symm_apply
 
 theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (M ≃ₗ[S] M₂) → M ≃ₗ[R] M₂) := fun _ _ h =>
@@ -708,7 +708,7 @@ def ofSubsingleton : M ≃ₗ[R] M₂ :=
     left_inv := fun _ => Subsingleton.elim _ _
     right_inv := fun _ => Subsingleton.elim _ _ }
 #align linear_equiv.of_subsingleton LinearEquiv.ofSubsingleton
-#align linear_equiv.of_subsingleton_symm_apply LinearEquiv.ofSubsingleton_symmApply
+#align linear_equiv.of_subsingleton_symm_apply LinearEquiv.ofSubsingleton_symm_apply
 
 @[simp]
 theorem ofSubsingleton_self : ofSubsingleton M M = refl R M := by
@@ -735,7 +735,7 @@ def compHom.toLinearEquiv {R S : Type _} [Semiring R] [Semiring S] (g : R ≃+*
     invFun := (g.symm : S → R)
     map_smul' := g.map_mul }
 #align module.comp_hom.to_linear_equiv Module.compHom.toLinearEquiv
-#align module.comp_hom.to_linear_equiv_symm_apply Module.compHom.toLinearEquiv_symmApply
+#align module.comp_hom.to_linear_equiv_symm_apply Module.compHom.toLinearEquiv_symm_apply
 
 end Module
 
@@ -753,7 +753,7 @@ def toLinearEquiv (s : S) : M ≃ₗ[R] M :=
   { toAddEquiv M s, toLinearMap R M s with }
 #align distrib_mul_action.to_linear_equiv DistribMulAction.toLinearEquiv
 #align distrib_mul_action.to_linear_equiv_apply DistribMulAction.toLinearEquiv_apply
-#align distrib_mul_action.to_linear_equiv_symm_apply DistribMulAction.toLinearEquiv_symmApply
+#align distrib_mul_action.to_linear_equiv_symm_apply DistribMulAction.toLinearEquiv_symm_apply
 
 /-- Each element of the group defines a module automorphism.
 

Mathlib/Algebra/Module/LinearMap.lean

@@ -1255,7 +1255,7 @@ def moduleEndSelfOp : R ≃+* Module.End Rᵐᵒᵖ R :=
     left_inv := mul_one
     right_inv := fun _ ↦ LinearMap.ext_ring_op <| mul_one _ }
 #align module.module_End_self_op Module.moduleEndSelfOp
-#align module.module_End_self_op_symm_apply Module.moduleEndSelfOp_symmApply
+#align module.module_End_self_op_symm_apply Module.moduleEndSelfOp_symm_apply
 #align module.module_End_self_op_apply Module.moduleEndSelfOp_apply
 
 theorem End.natCast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] :

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -456,7 +456,7 @@ def restrictScalarsEquiv (p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p :
     invFun := id
     map_smul' := fun _ _ => rfl }
 #align submodule.restrict_scalars_equiv Submodule.restrictScalarsEquiv
-#align submodule.restrict_scalars_equiv_symm_apply Submodule.restrictScalarsEquiv_symmApply
+#align submodule.restrict_scalars_equiv_symm_apply Submodule.restrictScalarsEquiv_symm_apply
 
 end RestrictScalars
 

Mathlib/Algebra/Module/ULift.lean

@@ -168,7 +168,7 @@ instance module' [Semiring R] [AddCommMonoid M] [Module R M] : Module R (ULift M
 #align ulift.module' ULift.module'
 
 /-- The `R`-linear equivalence between `ULift M` and `M`. -/
-@[simps apply symmApply]
+@[simps apply symm_apply]
 def moduleEquiv [Semiring R] [AddCommMonoid M] [Module R M] : ULift.{w} M ≃ₗ[R] M where
   toFun := ULift.down
   invFun := ULift.up

Mathlib/Algebra/Order/Field/Basic.lean

@@ -31,15 +31,15 @@ variable [LinearOrderedSemifield α] {a b c d e : α} {m n : ℤ}
 def OrderIso.mulLeft₀ (a : α) (ha : 0 < a) : α ≃o α :=
   { Equiv.mulLeft₀ a ha.ne' with map_rel_iff' := @fun _ _ => mul_le_mul_left ha }
 #align order_iso.mul_left₀ OrderIso.mulLeft₀
-#align order_iso.mul_left₀_symm_apply OrderIso.mulLeft₀_symmApply
+#align order_iso.mul_left₀_symm_apply OrderIso.mulLeft₀_symm_apply
 #align order_iso.mul_left₀_apply OrderIso.mulLeft₀_apply
 
 /-- `Equiv.mulRight₀` as an order_iso. -/
 @[simps! (config := { simpRhs := true })]
 def OrderIso.mulRight₀ (a : α) (ha : 0 < a) : α ≃o α :=
   { Equiv.mulRight₀ a ha.ne' with map_rel_iff' := @fun _ _ => mul_le_mul_right ha }
 #align order_iso.mul_right₀ OrderIso.mulRight₀
-#align order_iso.mul_right₀_symm_apply OrderIso.mulRight₀_symmApply
+#align order_iso.mul_right₀_symm_apply OrderIso.mulRight₀_symm_apply
 #align order_iso.mul_right₀_apply OrderIso.mulRight₀_apply
 
 /-!