chore: tidy various files (#2999)

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -18,7 +18,7 @@ import Mathlib.RingTheory.Ideal.Operations
 
 In this file we define `Subalgebra`s and the usual operations on them (`map`, `comap`).
 
-More lemmas about `adjoin` can be found in `ring_theory.adjoin`.
+More lemmas about `adjoin` can be found in `RingTheory.Adjoin`.
 -/
 
 
@@ -1080,8 +1080,7 @@ theorem coe_inclusion {S T : Subalgebra R A} (h : S ≤ T) (s : S) : (inclusion
 This is the `Subalgebra` version of `LinearEquiv.ofEq` and `Equiv.Set.ofEq`. -/
 @[simps apply]
 def equivOfEq (S T : Subalgebra R A) (h : S = T) : S ≃ₐ[R] T :=
-  { LinearEquiv.ofEq _ _
-      (congr_arg toSubmodule h) with
+  { LinearEquiv.ofEq _ _ (congr_arg toSubmodule h) with
     toFun := fun x => ⟨x, h ▸ x.2⟩
     invFun := fun x => ⟨x, h.symm ▸ x.2⟩
     map_mul' := fun _ _ => rfl
@@ -1106,15 +1105,13 @@ section Prod
 
 variable (S₁ : Subalgebra R B)
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /-- The product of two subalgebras is a subalgebra. -/
 def prod : Subalgebra R (A × B) :=
   { S.toSubsemiring.prod S₁.toSubsemiring with
     carrier := S ×ˢ S₁
     algebraMap_mem' := fun _ => ⟨algebraMap_mem _ _, algebraMap_mem _ _⟩ }
 #align subalgebra.prod Subalgebra.prod
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 @[simp]
 theorem coe_prod : (prod S S₁ : Set (A × B)) = S ×ˢ S₁ :=
   rfl
@@ -1242,7 +1239,7 @@ end SuprLift
 /-! ## Actions by `Subalgebra`s
 
 These are just copies of the definitions about `Subsemiring` starting from
-`subring.mul_action`.
+`Subring.mulAction`.
 -/
 
 
@@ -1257,15 +1254,15 @@ instance [SMul A α] (S : Subalgebra R A) : SMul S α :=
 theorem smul_def [SMul A α] {S : Subalgebra R A} (g : S) (m : α) : g • m = (g : A) • m := rfl
 #align subalgebra.smul_def Subalgebra.smul_def
 
-instance sMulCommClass_left [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) :
+instance smulCommClass_left [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) :
     SMulCommClass S α β :=
   S.toSubsemiring.smulCommClass_left
-#align subalgebra.smul_comm_class_left Subalgebra.sMulCommClass_left
+#align subalgebra.smul_comm_class_left Subalgebra.smulCommClass_left
 
-instance sMulCommClass_right [SMul α β] [SMul A β] [SMulCommClass α A β] (S : Subalgebra R A) :
+instance smulCommClass_right [SMul α β] [SMul A β] [SMulCommClass α A β] (S : Subalgebra R A) :
     SMulCommClass α S β :=
   S.toSubsemiring.smulCommClass_right
-#align subalgebra.smul_comm_class_right Subalgebra.sMulCommClass_right
+#align subalgebra.smul_comm_class_right Subalgebra.smulCommClass_right
 
 /-- Note that this provides `IsScalarTower S R R` which is needed by `smul_mul_assoc`. -/
 instance isScalarTower_left [SMul α β] [SMul A α] [SMul A β] [IsScalarTower A α β]

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -76,9 +76,9 @@ instance addSubmonoidClass : AddSubmonoidClass (Submodule R M) M where
   add_mem := AddSubsemigroup.add_mem' _
 #align submodule.add_submonoid_class Submodule.addSubmonoidClass
 
-instance subModuleClass : SubmoduleClass (Submodule R M) R M where
+instance submoduleClass : SubmoduleClass (Submodule R M) R M where
   smul_mem {s} c _ h := SubMulAction.smul_mem' s.toSubMulAction c h
-#align submodule.submodule_class Submodule.subModuleClass
+#align submodule.submodule_class Submodule.submoduleClass
 
 @[simp]
 theorem mem_toAddSubmonoid (p : Submodule R M) (x : M) : x ∈ p.toAddSubmonoid ↔ x ∈ p :=

Mathlib/Analysis/Normed/Group/Hom.lean

@@ -632,7 +632,7 @@ theorem sum_apply {ι : Type _} (s : Finset ι) (f : ι → NormedAddGroupHom V
 /-! ### Module structure on normed group homs -/
 
 
-instance distribMulActoin {R : Type _} [MonoidWithZero R] [DistribMulAction R V₂]
+instance distribMulAction {R : Type _} [MonoidWithZero R] [DistribMulAction R V₂]
     [PseudoMetricSpace R] [BoundedSMul R V₂] : DistribMulAction R (NormedAddGroupHom V₁ V₂) :=
   Function.Injective.distribMulAction coeAddHom coe_injective coe_smul
 

Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean

@@ -146,10 +146,10 @@ def coprodZeroIso (X : C) : X ⨿ (0 : C) ≅ X :=
 #align category_theory.limits.coprod_zero_iso CategoryTheory.Limits.coprodZeroIso
 
 @[simp]
-theorem inr_coprod_zeroiso_hom (X : C) : coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X := by
+theorem inr_coprodZeroIso_hom (X : C) : coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X := by
   dsimp [coprodZeroIso, binaryCofanZeroRight]
   simp
-#align category_theory.limits.inr_coprod_zeroiso_hom CategoryTheory.Limits.inr_coprod_zeroiso_hom
+#align category_theory.limits.inr_coprod_zeroiso_hom CategoryTheory.Limits.inr_coprodZeroIso_hom
 
 @[simp]
 theorem coprodZeroIso_inv (X : C) : (coprodZeroIso X).inv = coprod.inl :=