diff --git a/Archive/Imo/Imo2008Q4.lean b/Archive/Imo/Imo2008Q4.lean
index 10a8fc128a00b..0ea6215fb9966 100644
--- a/Archive/Imo/Imo2008Q4.lean
+++ b/Archive/Imo/Imo2008Q4.lean
@@ -83,7 +83,7 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
   specialize h₃ (a * b) hab
   cases' h₃ with hab₁ hab₂
   -- f(ab) = ab → b^4 = 1 → b = 1 → f(b) = b → false
-  · rw [ hab₁, div_left_inj' h2ab_ne_0 ] at H₂
+  · rw [hab₁, div_left_inj' h2ab_ne_0] at H₂
     field_simp at H₂
     have hb₁ : b ^ 4 = 1 := by linear_combination -H₂
     obtain hb₂ := abs_eq_one_of_pow_eq_one b 4 (show 4 ≠ 0 by norm_num) hb₁
diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
index e99949f30354f..9ace981fb076a 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@@ -123,7 +123,7 @@ lemma comp_app (f : P ⟶ Q) (g : Q ⟶ T) (X : Cᵒᵖ) :
 
 @[ext]
 theorem ext {f g : P ⟶ Q} (w : ∀ X, f.app X = g.app X) : f = g := by
-  cases f; cases g;
+  cases f; cases g
   congr
   ext X x
   exact LinearMap.congr_fun (w X) x
diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean
index dbf064901ad42..52138e37f626b 100644
--- a/Mathlib/Algebra/Module/LocalizedModule.lean
+++ b/Mathlib/Algebra/Module/LocalizedModule.lean
@@ -147,8 +147,8 @@ theorem zero_mk (s : S) : mk (0 : M) s = 0 :=
   mk_eq.mpr ⟨1, by rw [one_smul, smul_zero, smul_zero, one_smul]⟩
 #align localized_module.zero_mk LocalizedModule.zero_mk
 
-instance : Add (LocalizedModule S M)
-    where add p1 p2 :=
+instance : Add (LocalizedModule S M) where
+  add p1 p2 :=
     liftOn₂ p1 p2 (fun x y => mk (y.2 • x.1 + x.2 • y.1) (x.2 * y.2)) <|
       fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨m1', s1'⟩ ⟨m2', s2'⟩ ⟨u1, hu1⟩ ⟨u2, hu2⟩ =>
           mk_eq.mpr
@@ -196,8 +196,8 @@ private theorem add_zero' (x : LocalizedModule S M) : x + 0 = x :=
         exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
     x
 
-instance hasNatSmul : SMul ℕ (LocalizedModule S M) where smul n := nsmulRec n
-#align localized_module.has_nat_smul LocalizedModule.hasNatSmul
+instance hasNatSMul : SMul ℕ (LocalizedModule S M) where smul n := nsmulRec n
+#align localized_module.has_nat_smul LocalizedModule.hasNatSMul
 
 private theorem nsmul_zero' (x : LocalizedModule S M) : (0 : ℕ) • x = 0 :=
   LocalizedModule.induction_on (fun _ _ => rfl) x
@@ -294,8 +294,8 @@ instance {A : Type*} [CommSemiring A] [Algebra R A] {S : Submonoid R} :
 
 instance {A : Type} [Ring A] [Algebra R A] {S : Submonoid R} :
     Ring (LocalizedModule S A) :=
-    { inferInstanceAs (AddCommGroup (LocalizedModule S A)),
-      inferInstanceAs (Semiring (LocalizedModule S A)) with }
+  { inferInstanceAs (AddCommGroup (LocalizedModule S A)),
+    inferInstanceAs (Semiring (LocalizedModule S A)) with }
 
 instance {A : Type _} [CommRing A] [Algebra R A] {S : Submonoid R} :
     CommRing (LocalizedModule S A) :=
@@ -309,8 +309,8 @@ theorem mk_mul_mk {A : Type*} [Semiring A] [Algebra R A] {a₁ a₂ : A} {s₁ s
   rfl
 #align localized_module.mk_mul_mk LocalizedModule.mk_mul_mk
 
-instance : SMul (Localization S) (LocalizedModule S M)
-    where smul f x :=
+instance : SMul (Localization S) (LocalizedModule S M) where
+  smul f x :=
     (Localization.liftOn f
       (fun r s =>
         (liftOn x (fun p => (mk (r • p.1) (s * p.2)))
@@ -450,8 +450,7 @@ instance : IsScalarTower R (Localization S) (LocalizedModule S M) :=
 
 instance algebra' {A : Type*} [Semiring A] [Algebra R A] : Algebra R (LocalizedModule S A) :=
   { (algebraMap (Localization S) (LocalizedModule S A)).comp (algebraMap R <| Localization S),
-    show Module R (LocalizedModule S A) by
-      infer_instance with
+    show Module R (LocalizedModule S A) by infer_instance with
     commutes' := by
       intro r x
       obtain ⟨⟨a, s⟩, rfl : mk a s = x⟩ := Quotient.exists_rep x
@@ -577,13 +576,12 @@ noncomputable def lift' (g : M →ₗ[R] M'')
   fun m =>
   m.liftOn (fun p => (h p.2).unit⁻¹.val <| g p.1) fun ⟨m, s⟩ ⟨m', s'⟩ ⟨c, eq1⟩ => by
     -- Porting note: We remove `generalize_proofs h1 h2`. This does nothing here.
-    erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← map_smul]
-    symm
-    erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff]
-    dsimp
+    dsimp only
+    simp only [Submonoid.smul_def] at eq1
+    rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, eq_comm,
+      Module.End_algebraMap_isUnit_inv_apply_eq_iff]
     have : c • s • g m' = c • s' • g m := by
-      erw [← g.map_smul, ← g.map_smul, ← g.map_smul, ← g.map_smul, eq1]
-      rfl
+      simp only [Submonoid.smul_def, ← g.map_smul, eq1]
     have : Function.Injective (h c).unit.inv := by
       rw [Function.injective_iff_hasLeftInverse]
       refine' ⟨(h c).unit, _⟩
@@ -594,9 +592,8 @@ noncomputable def lift' (g : M →ₗ[R] M'')
     erw [Units.inv_eq_val_inv, Module.End_algebraMap_isUnit_inv_apply_eq_iff, ←
       (h c).unit⁻¹.val.map_smul]
     symm
-    erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
+    rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
       g.map_smul, eq1]
-    rfl
 #align localized_module.lift' LocalizedModule.lift'
 
 theorem lift'_mk (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
@@ -659,7 +656,7 @@ theorem lift_mk
 
 /--
 If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
-there is a linear map `lift g ∘ mk_linear_map = g`.
+there is a linear map `lift g ∘ mkLinearMap = g`.
 -/
 theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
     (lift S g h).comp (mkLinearMap S M) = g := by
@@ -669,7 +666,7 @@ theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (M
 
 /--
 If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible and
-`l` is another linear map `LocalizedModule S M ⟶ M''` such that `l ∘ mk_linear_map = g` then
+`l` is another linear map `LocalizedModule S M ⟶ M''` such that `l ∘ mkLinearMap = g` then
 `l = lift g`
 -/
 theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
@@ -677,10 +674,10 @@ theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R
     LocalizedModule.lift S g h = l := by
   ext x; induction' x using LocalizedModule.induction_on with m s
   rw [LocalizedModule.lift_mk]
-  erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
+  rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
     Function.comp_apply, LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_mk]
   congr 1; rw [LocalizedModule.mk_eq]
-  refine' ⟨1, _⟩; simp only [one_smul]; rfl
+  refine' ⟨1, _⟩; simp only [one_smul, Submonoid.smul_def]
 #align localized_module.lift_unique LocalizedModule.lift_unique
 
 end LocalizedModule
@@ -743,7 +740,7 @@ theorem fromLocalizedModule'_add (x y : LocalizedModule S M) :
       erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, smul_add, ←map_smul, ←map_smul,
         ←map_smul, map_add]
       congr 1
-      all_goals erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff']
+      all_goals rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff']
       · erw [mul_smul, f.map_smul]
         rfl
       · erw [mul_comm, f.map_smul, mul_smul]
@@ -782,18 +779,18 @@ theorem fromLocalizedModule.inj : Function.Injective <| fromLocalizedModule S f
   induction' y using LocalizedModule.induction_on with a' b'
   simp only [fromLocalizedModule_mk] at eq1
   -- Porting note: We remove `generalize_proofs h1 h2`.
-  erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← LinearMap.map_smul,
+  rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← LinearMap.map_smul,
     Module.End_algebraMap_isUnit_inv_apply_eq_iff'] at eq1
   erw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f,
     f.map_smul, f.map_smul, eq1]
-  rfl
+  rw [Submonoid.coe_subtype]
 #align is_localized_module.from_localized_module.inj IsLocalizedModule.fromLocalizedModule.inj
 
 theorem fromLocalizedModule.surj : Function.Surjective <| fromLocalizedModule S f := fun x =>
   let ⟨⟨m, s⟩, eq1⟩ := IsLocalizedModule.surj S f x
   ⟨LocalizedModule.mk m s, by
-    rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← eq1]
-    rfl⟩
+    rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
+      Submonoid.smul_def]⟩
 #align is_localized_module.from_localized_module.surj IsLocalizedModule.fromLocalizedModule.surj
 
 theorem fromLocalizedModule.bij : Function.Bijective <| fromLocalizedModule S f :=
@@ -853,9 +850,7 @@ noncomputable def lift (g : M →ₗ[R] M'')
 theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
     (lift S f g h).comp f = g := by
   dsimp only [IsLocalizedModule.lift]
-  rw [LinearMap.comp_assoc]
-  convert LocalizedModule.lift_comp S g h
-  exact iso_symm_comp _ _
+  rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]
 #align is_localized_module.lift_comp IsLocalizedModule.lift_comp
 
 theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
@@ -868,7 +863,9 @@ theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R
   · rw [LinearMap.comp_assoc, ← hl]
     congr 1
     ext x
-    erw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, one_smul]
+    rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe, iso_apply,
+      fromLocalizedModule'_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one,
+      one_smul]
 #align is_localized_module.lift_unique IsLocalizedModule.lift_unique
 
 /-- Universal property from localized module:
@@ -948,8 +945,8 @@ variable {S}
 @[simp]
 theorem mk'_cancel (m : M) (s : S) : mk' f (s • m) s = f m := by
   delta mk'
-  rw [LocalizedModule.mk_cancel, ← mk'_one S f]
-  rfl
+  rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
+    Module.End_algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
 #align is_localized_module.mk'_cancel IsLocalizedModule.mk'_cancel
 
 @[simp]
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
index 6e831017f254a..f9482f6e50396 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
@@ -34,7 +34,7 @@ namespace AlgebraicGeometry
 variable {X Y : Scheme.{u}} (f : X ⟶ Y)
 
 /--
-A morphism is `quasi-compact` if the underlying map of topological spaces is, i.e. if the preimages
+A morphism is "quasi-compact" if the underlying map of topological spaces is, i.e. if the preimages
 of quasi-compact open sets are quasi-compact.
 -/
 @[mk_iff]
@@ -47,7 +47,7 @@ theorem quasiCompact_iff_spectral : QuasiCompact f ↔ IsSpectralMap f.1.base :=
   ⟨fun ⟨h⟩ => ⟨by continuity, h⟩, fun h => ⟨h.2⟩⟩
 #align algebraic_geometry.quasi_compact_iff_spectral AlgebraicGeometry.quasiCompact_iff_spectral
 
-/-- The `affine_target_morphism_property` corresponding to `quasi_compact`, asserting that the
+/-- The `AffineTargetMorphismProperty` corresponding to `QuasiCompact`, asserting that the
 domain is a quasi-compact scheme. -/
 def QuasiCompact.affineProperty : AffineTargetMorphismProperty := fun X _ _ _ =>
   CompactSpace X.carrier
@@ -181,7 +181,7 @@ theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _).
       topIsAffineOpen _]
 #align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal
 
-theorem QuasiCompact.affine_openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
+theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
     List.TFAE
       [QuasiCompact f,
         ∃ (𝒰 : Scheme.OpenCover.{u} Y) (_ : ∀ i, IsAffine (𝒰.obj i)),
@@ -193,14 +193,14 @@ theorem QuasiCompact.affine_openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
         ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤) (_ : ∀ i, IsAffineOpen (U i)),
           ∀ i, CompactSpace (f.1.base ⁻¹' (U i).1)] :=
   quasiCompact_eq_affineProperty.symm ▸ QuasiCompact.affineProperty_isLocal.affine_openCover_TFAE f
-#align algebraic_geometry.quasi_compact.affine_open_cover_tfae AlgebraicGeometry.QuasiCompact.affine_openCover_tFAE
+#align algebraic_geometry.quasi_compact.affine_open_cover_tfae AlgebraicGeometry.QuasiCompact.affine_openCover_tfae
 
 theorem QuasiCompact.is_local_at_target : PropertyIsLocalAtTarget @QuasiCompact :=
   quasiCompact_eq_affineProperty.symm ▸
     QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal
 #align algebraic_geometry.quasi_compact.is_local_at_target AlgebraicGeometry.QuasiCompact.is_local_at_target
 
-theorem QuasiCompact.openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
+theorem QuasiCompact.openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
     List.TFAE
       [QuasiCompact f,
         ∃ 𝒰 : Scheme.OpenCover.{u} Y,
@@ -213,7 +213,7 @@ theorem QuasiCompact.openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
         ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤), ∀ i, QuasiCompact (f ∣_ U i)] :=
   quasiCompact_eq_affineProperty.symm ▸
     QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal.openCover_TFAE f
-#align algebraic_geometry.quasi_compact.open_cover_tfae AlgebraicGeometry.QuasiCompact.openCover_tFAE
+#align algebraic_geometry.quasi_compact.open_cover_tfae AlgebraicGeometry.QuasiCompact.openCover_tfae
 
 theorem quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
     QuasiCompact f ↔ CompactSpace X.carrier :=
@@ -250,7 +250,6 @@ theorem QuasiCompact.affineProperty_stableUnderBaseChange :
     QuasiCompact.affineProperty.StableUnderBaseChange := by
   intro X Y S _ _ f g h
   rw [QuasiCompact.affineProperty] at h ⊢
-  skip
   let 𝒰 := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
   have : Finite 𝒰.J := by dsimp; infer_instance
   have : ∀ i, CompactSpace (𝒰.obj i).carrier := by intro i; dsimp; infer_instance
diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean
index 863930baaaddf..e7c7f64c23d55 100644
--- a/Mathlib/Analysis/Calculus/Taylor.lean
+++ b/Mathlib/Analysis/Calculus/Taylor.lean
@@ -285,7 +285,7 @@ theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ
   use y, hy
   simp only [sub_self, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h
   rw [h, neg_div, ← div_neg, neg_mul, neg_neg]
-  field_simp [xy_ne y hy];  ring
+  field_simp [xy_ne y hy]; ring
 #align taylor_mean_remainder_lagrange taylor_mean_remainder_lagrange
 
 /-- **Taylor's theorem** with the Cauchy form of the remainder.
diff --git a/Mathlib/Analysis/Convex/Normed.lean b/Mathlib/Analysis/Convex/Normed.lean
index ec88b396f4932..7dbd4143c324a 100644
--- a/Mathlib/Analysis/Convex/Normed.lean
+++ b/Mathlib/Analysis/Convex/Normed.lean
@@ -120,14 +120,14 @@ theorem bounded_convexHull {s : Set E} : Metric.Bounded (convexHull ℝ s) ↔ M
   simp only [Metric.bounded_iff_ediam_ne_top, convexHull_ediam]
 #align bounded_convex_hull bounded_convexHull
 
-instance (priority := 100) NormedSpace.path_connected : PathConnectedSpace E :=
+instance (priority := 100) NormedSpace.instPathConnectedSpace : PathConnectedSpace E :=
   TopologicalAddGroup.pathConnectedSpace
-#align normed_space.path_connected NormedSpace.path_connected
+#align normed_space.path_connected NormedSpace.instPathConnectedSpace
 
-instance (priority := 100) NormedSpace.loc_path_connected : LocPathConnectedSpace E :=
+instance (priority := 100) NormedSpace.instLocPathConnectedSpace : LocPathConnectedSpace E :=
   locPathConnected_of_bases (fun x => Metric.nhds_basis_ball) fun x r r_pos =>
     (convex_ball x r).isPathConnected <| by simp [r_pos]
-#align normed_space.loc_path_connected NormedSpace.loc_path_connected
+#align normed_space.loc_path_connected NormedSpace.instLocPathConnectedSpace
 
 theorem dist_add_dist_of_mem_segment {x y z : E} (h : y ∈ [x -[ℝ] z]) :
     dist x y + dist y z = dist x z := by
diff --git a/Mathlib/Analysis/LocallyConvex/Barrelled.lean b/Mathlib/Analysis/LocallyConvex/Barrelled.lean
index a923c78e1f2e8..f2f06a246d96a 100644
--- a/Mathlib/Analysis/LocallyConvex/Barrelled.lean
+++ b/Mathlib/Analysis/LocallyConvex/Barrelled.lean
@@ -173,7 +173,7 @@ protected theorem banach_steinhaus (H : ∀ k x, BddAbove (range fun i ↦ q k (
 domain is barrelled, the Banach-Steinhaus theorem is used to guarantee that the limit map
 is a *continuous* linear map as well.
 
-This actually works for any *countably generated* filter instead of `AtTop : Filter ℕ`,
+This actually works for any *countably generated* filter instead of `atTop : Filter ℕ`,
 but the proof ultimately goes back to sequences. -/
 protected def continuousLinearMapOfTendsto [T2Space F] {l : Filter α} [l.IsCountablyGenerated]
     [l.NeBot] (g : α → E →SL[σ₁₂] F) {f : E → F} (h : Tendsto (fun n x ↦ g n x) l (𝓝 f)) :
@@ -182,7 +182,7 @@ protected def continuousLinearMapOfTendsto [T2Space F] {l : Filter α} [l.IsCoun
   cont := by
     -- Since the filter `l` is countably generated and nontrivial, we can find a sequence
     -- `u : ℕ → α` that tends to `l`. By considering `g ∘ u` instead of `g`, we can thus assume
-    -- that `α = ℕ` and `l = AtTop`
+    -- that `α = ℕ` and `l = atTop`
     rcases l.exists_seq_tendsto with ⟨u, hu⟩
     -- We claim that the limit is continuous because it's a limit of an equicontinuous family.
     -- By the Banach-Steinhaus theorem, this equicontinuity will follow from pointwise boundedness.
diff --git a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
index 2bd508d07b580..57881e086b159 100644
--- a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
+++ b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
@@ -460,7 +460,7 @@ variable [Limits.HasPullbacks C]
     that `f p = g q`, then there is some `s : pullback f g` such that `fst s = p` and `snd s = q`.
 
     Remark: Borceux claims that `s` is unique, but this is false. See
-    `Counterexamples/Pseudoelement` for details. -/
+    `Counterexamples/Pseudoelement.lean` for details. -/
 theorem pseudo_pullback {P Q R : C} {f : P ⟶ R} {g : Q ⟶ R} {p : P} {q : Q} :
     f p = g q →
       ∃ s, (pullback.fst : pullback f g ⟶ P) s = p ∧ (pullback.snd : pullback f g ⟶ Q) s = q :=
diff --git a/Mathlib/CategoryTheory/Bicategory/Adjunction.lean b/Mathlib/CategoryTheory/Bicategory/Adjunction.lean
index aeedbdb3c23b1..e0f0b03be5714 100644
--- a/Mathlib/CategoryTheory/Bicategory/Adjunction.lean
+++ b/Mathlib/CategoryTheory/Bicategory/Adjunction.lean
@@ -77,9 +77,9 @@ def rightZigzag (η : 𝟙 a ⟶ f ≫ g) (ε : g ≫ f ⟶ 𝟙 b) :=
 
 /-- Adjunction between two 1-morphisms. -/
 structure Adjunction (f : a ⟶ b) (g : b ⟶ a) where
-  /-- The unit of an adjuntion. -/
+  /-- The unit of an adjunction. -/
   unit : 𝟙 a ⟶ f ≫ g
-  /-- The counit of an adjuntion. -/
+  /-- The counit of an adjunction. -/
   counit : g ≫ f ⟶ 𝟙 b
   /-- The composition of the unit and the counit is equal to the identity up to unitors. -/
   left_triangle : leftZigzag unit counit = (λ_ _).hom ≫ (ρ_ _).inv := by aesop_cat
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
index 683649fc65925..34d4c80d00696 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
@@ -111,9 +111,8 @@ lemma _root_.SimpleGraph.Walk.toSubgraph_connected {u v : V} (p : G.Walk u v) :
     p.toSubgraph.Connected := by
   induction p with
   | nil => apply singletonSubgraph_connected
-  | cons h p ih =>
+  | @cons _ w _ h p ih =>
     apply (subgraphOfAdj_connected h).sup ih
-    rename_i w _
     exists w
     simp
 
@@ -148,8 +147,9 @@ lemma preconnected_iff_forall_exists_walk_subgraph (H : G.Subgraph) :
       (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)
 
 lemma connected_iff_forall_exists_walk_subgraph (H : G.Subgraph) :
-    H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v}, u ∈ H.verts → v ∈ H.verts →
-                                        ∃ p : G.Walk u v, p.toSubgraph ≤ H := by
+    H.Connected ↔
+      H.verts.Nonempty ∧
+        ∀ {u v}, u ∈ H.verts → v ∈ H.verts → ∃ p : G.Walk u v, p.toSubgraph ≤ H := by
   rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]
 
 end Subgraph
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 30d2c53c19cb4..d0863402bd750 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -283,7 +283,7 @@ end InsertErase
 
 section SmallSets
 
-theorem encard_pair (hne : x ≠ y) : ({x,y} : Set α).encard = 2 := by
+theorem encard_pair (hne : x ≠ y) : ({x, y} : Set α).encard = 2 := by
   rw [encard_insert_of_not_mem (by simpa), ←one_add_one_eq_two,
     WithTop.add_right_cancel_iff WithTop.one_ne_top, encard_singleton]
 
@@ -308,11 +308,11 @@ theorem one_lt_encard_iff : 1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a
 
 theorem exists_ne_of_one_lt_encard (h : 1 < s.encard) (a : α) : ∃ b ∈ s, b ≠ a := by
   by_contra' h'
-  obtain ⟨b,b',hb,hb',hne⟩ := one_lt_encard_iff.1 h
+  obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h
   apply hne
   rw [h' b hb, h' b' hb']
 
-theorem encard_eq_two : s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x,y} := by
+theorem encard_eq_two : s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} := by
   refine' ⟨fun h ↦ _, fun ⟨x, y, hne, hs⟩ ↦ by rw [hs, encard_pair hne]⟩
   obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
   rw [←insert_eq_of_mem hx, ←insert_diff_singleton, encard_insert_of_not_mem (fun h ↦ h.2 rfl),
@@ -328,8 +328,8 @@ theorem encard_eq_three {α : Type u_1} {s : Set α} :
     rw [←insert_eq_of_mem hx, ←insert_diff_singleton,
       encard_insert_of_not_mem (fun h ↦ h.2 rfl), (by exact rfl : (3 : ℕ∞) = 2 + 1),
       WithTop.add_right_cancel_iff WithTop.one_ne_top, encard_eq_two] at h
-    obtain ⟨y,z,hne, hs⟩ := h
-    refine' ⟨x,y,z, _, _, hne, _⟩
+    obtain ⟨y, z, hne, hs⟩ := h
+    refine' ⟨x, y, z, _, _, hne, _⟩
     · rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
     · rintro rfl; exact (hs.symm.subset (Or.inr rfl)).2 rfl
     rw [←hs, insert_diff_singleton, insert_eq_of_mem hx]
@@ -360,7 +360,7 @@ theorem exists_subset_encard_eq (hk : k ≤ s.encard) : ∃ t, t ⊆ s ∧ t.enc
   simp only [top_le_iff, encard_eq_top_iff]
   exact fun _ hi ↦ ⟨s, Subset.rfl, hi⟩
 
-theorem exists_supset_subset_encard_eq (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) :
+theorem exists_superset_subset_encard_eq (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) :
     ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k := by
   obtain (hs | hs) := eq_or_ne s.encard ⊤
   · rw [hs, top_le_iff] at hsk; subst hsk; exact ⟨s, Subset.rfl, hst, hs⟩
@@ -434,7 +434,7 @@ theorem Finite.exists_injOn_of_encard_le [Nonempty β] {s : Set α} {t : Set β}
     mem_insert_iff, mem_preimage, ne_eq, Function.update_apply, forall_eq_or_imp, ite_true, and_imp,
     mem_image, ite_eq_left_iff, not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]
 
-  refine ⟨?_,?_,fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
+  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
   · rintro x hx; split_ifs with h; assumption; exact (hf₀s x hx h).1
   exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_noteq])
 termination_by _ => encard s
@@ -908,22 +908,19 @@ theorem ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff (hs : s.Finite := by toFinit
     (ht : t.Finite := by toFinite_tac) : s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard := by
   rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
     inter_comm, add_right_inj]
-#align set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff
-  Set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff
+#align set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff Set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff
 
 theorem ncard_le_ncard_iff_ncard_diff_le_ncard_diff (hs : s.Finite := by toFinite_tac)
     (ht : t.Finite := by toFinite_tac) : s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard := by
   rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
     inter_comm, add_le_add_iff_left]
-#align set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff
-  Set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff
+#align set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff Set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff
 
 theorem ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff (hs : s.Finite := by toFinite_tac)
     (ht : t.Finite := by toFinite_tac) : s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard := by
   rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
     inter_comm, add_lt_add_iff_left]
-#align set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff
-  Set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff
+#align set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff Set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff
 
 theorem ncard_add_ncard_compl (s : Set α) (hs : s.Finite := by toFinite_tac)
     (hsc : sᶜ.Finite := by toFinite_tac) : s.ncard + sᶜ.ncard = Nat.card α := by
@@ -972,13 +969,13 @@ theorem Infinite.exists_subset_ncard_eq {s : Set α} (hs : s.Infinite) (k : ℕ)
   simp
 #align set.Infinite.exists_subset_ncard_eq Set.Infinite.exists_subset_ncard_eq
 
-theorem Infinite.exists_supset_ncard_eq {s t : Set α} (ht : t.Infinite) (hst : s ⊆ t)
+theorem Infinite.exists_superset_ncard_eq {s t : Set α} (ht : t.Infinite) (hst : s ⊆ t)
     (hs : s.Finite) {k : ℕ} (hsk : s.ncard ≤ k) : ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k := by
   obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)
   refine' ⟨s ∪ s₁, subset_union_left _ _, union_subset hst (hs₁.trans (diff_subset _ _)), _⟩
   rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
     add_tsub_cancel_of_le]
-#align set.infinite.exists_supset_ncard_eq Set.Infinite.exists_supset_ncard_eq
+#align set.infinite.exists_supset_ncard_eq Set.Infinite.exists_superset_ncard_eq
 
 theorem exists_subset_or_subset_of_two_mul_lt_ncard {n : ℕ} (hst : 2 * n < (s ∪ t).ncard) :
     ∃ r : Set α, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t) := by
@@ -1105,14 +1102,14 @@ theorem ncard_eq_two : s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} := by
   rw [←encard_eq_two, ncard_def, ←Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]
   refine' ⟨fun h ↦ _, fun h ↦ _⟩
   · rwa [ENat.coe_toNat] at h; rintro h'; simp [h'] at h
-  simp [h]; exact Iff.mp ENat.coe_toNat_eq_self rfl
+  rw [h]; rfl
 #align set.ncard_eq_two Set.ncard_eq_two
 
 theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} := by
   rw [←encard_eq_three, ncard_def, ←Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]
   refine' ⟨fun h ↦ _, fun h ↦ _⟩
   · rwa [ENat.coe_toNat] at h; rintro h'; simp [h'] at h
-  simp [h]; exact Iff.mp ENat.coe_toNat_eq_self rfl
+  rw [h]; rfl
 #align set.ncard_eq_three Set.ncard_eq_three
 
 end ncard
diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
index bd595e2eb5502..2ca5acce03943 100644
--- a/Mathlib/Data/Set/Function.lean
+++ b/Mathlib/Data/Set/Function.lean
@@ -1264,7 +1264,7 @@ theorem InjOn.invFunOn_image [Nonempty α] (h : InjOn f s₂) (ht : s₁ ⊆ s
   h.leftInvOn_invFunOn.image_image' ht
 #align set.inj_on.inv_fun_on_image Set.InjOn.invFunOn_image
 
-theorem _root_.Function.LeftInvOn_invFunOn_of_subset_image_image [Nonempty α]
+theorem _root_.Function.leftInvOn_invFunOn_of_subset_image_image [Nonempty α]
     (h : s ⊆ (invFunOn f s) '' (f '' s)) : LeftInvOn (invFunOn f s) f s :=
   fun x hx ↦ by
     obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
@@ -1273,7 +1273,7 @@ theorem _root_.Function.LeftInvOn_invFunOn_of_subset_image_image [Nonempty α]
 theorem injOn_iff_invFunOn_image_image_eq_self [Nonempty α] :
     InjOn f s ↔ (invFunOn f s) '' (f '' s) = s :=
   ⟨fun h ↦ h.invFunOn_image Subset.rfl, fun h ↦
-    (Function.LeftInvOn_invFunOn_of_subset_image_image h.symm.subset).injOn⟩
+    (Function.leftInvOn_invFunOn_of_subset_image_image h.symm.subset).injOn⟩
 
 theorem _root_.Function.invFunOn_injOn_image [Nonempty α] (f : α → β) (s : Set α) :
     Set.InjOn (invFunOn f s) (f '' s) := by
diff --git a/Mathlib/NumberTheory/ModularForms/Basic.lean b/Mathlib/NumberTheory/ModularForms/Basic.lean
index 61a34610df4bf..e0298e68531dd 100644
--- a/Mathlib/NumberTheory/ModularForms/Basic.lean
+++ b/Mathlib/NumberTheory/ModularForms/Basic.lean
@@ -14,7 +14,7 @@ import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
 
 This file defines modular forms and proves some basic properties about them.
 
-We begin by defining modular forms and cusp forms as extension of `slash_invariant_forms` then we
+We begin by defining modular forms and cusp forms as extension of `SlashInvariantForm`s then we
 define the space of modular forms, cusp forms and prove that the product of two modular forms is a
 modular form.
 -/
@@ -37,26 +37,26 @@ variable (F : Type*) (Γ : Subgroup SL(2, ℤ)) (k : ℤ)
 
 open scoped ModularForm
 
-/-- These are `slash_invariant_form`'s that are holomophic and bounded at infinity. -/
+/-- These are `SlashInvariantForm`'s that are holomophic and bounded at infinity. -/
 structure ModularForm extends SlashInvariantForm Γ k where
   holo' : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (toSlashInvariantForm : ℍ → ℂ)
   bdd_at_infty' : ∀ A : SL(2, ℤ), IsBoundedAtImInfty (toSlashInvariantForm ∣[k] A)
 #align modular_form ModularForm
 
-/-- The `slash_invariant_form` associated to a `modular_form`. -/
+/-- The `SlashInvariantForm` associated to a `ModularForm`. -/
 add_decl_doc ModularForm.toSlashInvariantForm
 
-/-- These are `slash_invariant_form`s that are holomophic and zero at infinity. -/
+/-- These are `SlashInvariantForm`s that are holomophic and zero at infinity. -/
 structure CuspForm extends SlashInvariantForm Γ k where
   holo' : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (toSlashInvariantForm : ℍ → ℂ)
   zero_at_infty' : ∀ A : SL(2, ℤ), IsZeroAtImInfty (toSlashInvariantForm ∣[k] A)
 #align cusp_form CuspForm
 
-/-- The `slash_invariant_form` associated to a `cusp_form`. -/
+/-- The `SlashInvariantForm` associated to a `CuspForm`. -/
 add_decl_doc CuspForm.toSlashInvariantForm
 
-/-- `modular_form_class F Γ k` says that `F` is a type of bundled functions that extend
-`slash_invariant_form_class` by requiring that the functions be holomorphic and bounded
+/-- `ModularFormClass F Γ k` says that `F` is a type of bundled functions that extend
+`SlashInvariantFormClass` by requiring that the functions be holomorphic and bounded
 at infinity. -/
 class ModularFormClass (F : Type*) (Γ : outParam <| Subgroup (SL(2, ℤ))) (k : outParam ℤ)
     extends SlashInvariantFormClass F Γ k where
@@ -64,8 +64,8 @@ class ModularFormClass (F : Type*) (Γ : outParam <| Subgroup (SL(2, ℤ))) (k :
   bdd_at_infty : ∀ (f : F) (A : SL(2, ℤ)), IsBoundedAtImInfty (f ∣[k] A)
 #align modular_form_class ModularFormClass
 
-/-- `cusp_form_class F Γ k` says that `F` is a type of bundled functions that extend
-`slash_invariant_form_class` by requiring that the functions be holomorphic and zero
+/-- `CuspFormClass F Γ k` says that `F` is a type of bundled functions that extend
+`SlashInvariantFormClass` by requiring that the functions be holomorphic and zero
 at infinity. -/
 class CuspFormClass (F : Type*) (Γ : outParam <| Subgroup (SL(2, ℤ))) (k : outParam ℤ)
     extends SlashInvariantFormClass F Γ k where
@@ -117,7 +117,7 @@ theorem CuspForm.ext {f g : CuspForm Γ k} (h : ∀ x, f x = g x) : f = g :=
   FunLike.ext f g h
 #align cusp_form.ext CuspForm.ext
 
-/-- Copy of a `modular_form` with a new `to_fun` equal to the old one. Useful to fix
+/-- Copy of a `ModularForm` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def ModularForm.copy (f : ModularForm Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) :
     ModularForm Γ k where
@@ -126,7 +126,7 @@ protected def ModularForm.copy (f : ModularForm Γ k) (f' : ℍ → ℂ) (h : f'
   bdd_at_infty' A := h.symm ▸ f.bdd_at_infty' A
 #align modular_form.copy ModularForm.copy
 
-/-- Copy of a `cusp_form` with a new `to_fun` equal to the old one. Useful to fix
+/-- Copy of a `CuspForm` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def CuspForm.copy (f : CuspForm Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) : CuspForm Γ k where
   toSlashInvariantForm := f.1.copy f' h
@@ -159,11 +159,11 @@ theorem add_apply (f g : ModularForm Γ k) (z : ℍ) : (f + g) z = f z + g z :=
   rfl
 #align modular_form.add_apply ModularForm.add_apply
 
-instance hasZero : Zero (ModularForm Γ k) :=
+instance instZero : Zero (ModularForm Γ k) :=
   ⟨ { toSlashInvariantForm := 0
       holo' := fun _ => mdifferentiableAt_const 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ)
       bdd_at_infty' := fun A => by simpa using zero_form_isBoundedAtImInfty } ⟩
-#align modular_form.has_zero ModularForm.hasZero
+#align modular_form.has_zero ModularForm.instZero
 
 @[simp]
 theorem coe_zero : ⇑(0 : ModularForm Γ k) = (0 : ℍ → ℂ) :=
@@ -179,12 +179,12 @@ section
 
 variable {α : Type*} [SMul α ℂ] [IsScalarTower α ℂ ℂ]
 
-instance hasSmul : SMul α (ModularForm Γ k) :=
+instance instSMul : SMul α (ModularForm Γ k) :=
   ⟨fun c f =>
     { toSlashInvariantForm := c • f.1
       holo' := by simpa using f.holo'.const_smul (c • (1 : ℂ))
       bdd_at_infty' := fun A => by simpa using (f.bdd_at_infty' A).const_smul_left (c • (1 : ℂ)) }⟩
-#align modular_form.has_smul ModularForm.hasSmul
+#align modular_form.has_smul ModularForm.instSMul
 
 @[simp]
 theorem coe_smul (f : ModularForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f :=
@@ -198,12 +198,12 @@ theorem smul_apply (f : ModularForm Γ k) (n : α) (z : ℍ) : (n • f) z = n 
 
 end
 
-instance hasNeg : Neg (ModularForm Γ k) :=
+instance instNeg : Neg (ModularForm Γ k) :=
   ⟨fun f =>
     { toSlashInvariantForm := -f.1
       holo' := f.holo'.neg
       bdd_at_infty' := fun A => by simpa using (f.bdd_at_infty' A).neg }⟩
-#align modular_form.has_neg ModularForm.hasNeg
+#align modular_form.has_neg ModularForm.instNeg
 
 @[simp]
 theorem coe_neg (f : ModularForm Γ k) : ⇑(-f) = -f :=
@@ -215,9 +215,9 @@ theorem neg_apply (f : ModularForm Γ k) (z : ℍ) : (-f) z = -f z :=
   rfl
 #align modular_form.neg_apply ModularForm.neg_apply
 
-instance hasSub : Sub (ModularForm Γ k) :=
+instance instSub : Sub (ModularForm Γ k) :=
   ⟨fun f g => f + -g⟩
-#align modular_form.has_sub ModularForm.hasSub
+#align modular_form.has_sub ModularForm.instSub
 
 @[simp]
 theorem coe_sub (f g : ModularForm Γ k) : ⇑(f - g) = f - g :=
@@ -232,7 +232,7 @@ theorem sub_apply (f g : ModularForm Γ k) (z : ℍ) : (f - g) z = f z - g z :=
 instance : AddCommGroup (ModularForm Γ k) :=
   FunLike.coe_injective.addCommGroup _ rfl coe_add coe_neg coe_sub coe_smul coe_smul
 
-/-- Additive coercion from `modular_form` to `ℍ → ℂ`. -/
+/-- Additive coercion from `ModularForm` to `ℍ → ℂ`. -/
 @[simps]
 def coeHom : ModularForm Γ k →+ ℍ → ℂ where
   toFun f := f
@@ -302,11 +302,11 @@ theorem add_apply (f g : CuspForm Γ k) (z : ℍ) : (f + g) z = f z + g z :=
   rfl
 #align cusp_form.add_apply CuspForm.add_apply
 
-instance hasZero : Zero (CuspForm Γ k) :=
+instance instZero : Zero (CuspForm Γ k) :=
   ⟨ { toSlashInvariantForm := 0
       holo' := fun _ => mdifferentiableAt_const 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ)
       zero_at_infty' := by simpa using Filter.zero_zeroAtFilter _ } ⟩
-#align cusp_form.has_zero CuspForm.hasZero
+#align cusp_form.has_zero CuspForm.instZero
 
 @[simp]
 theorem coe_zero : ⇑(0 : CuspForm Γ k) = (0 : ℍ → ℂ) :=
@@ -322,12 +322,12 @@ section
 
 variable {α : Type*} [SMul α ℂ] [IsScalarTower α ℂ ℂ]
 
-instance hasSmul : SMul α (CuspForm Γ k) :=
+instance instSMul : SMul α (CuspForm Γ k) :=
   ⟨fun c f =>
     { toSlashInvariantForm := c • f.1
       holo' := by simpa using f.holo'.const_smul (c • (1 : ℂ))
       zero_at_infty' := fun A => by simpa using (f.zero_at_infty' A).smul (c • (1 : ℂ)) }⟩
-#align cusp_form.has_smul CuspForm.hasSmul
+#align cusp_form.has_smul CuspForm.instSMul
 
 @[simp]
 theorem coe_smul (f : CuspForm Γ k) (n : α) : ⇑(n • f) = n • ⇑f :=
@@ -341,12 +341,12 @@ theorem smul_apply (f : CuspForm Γ k) (n : α) {z : ℍ} : (n • f) z = n •
 
 end
 
-instance hasNeg : Neg (CuspForm Γ k) :=
+instance instNeg : Neg (CuspForm Γ k) :=
   ⟨fun f =>
     { toSlashInvariantForm := -f.1
       holo' := f.holo'.neg
       zero_at_infty' := fun A => by simpa using (f.zero_at_infty' A).neg }⟩
-#align cusp_form.has_neg CuspForm.hasNeg
+#align cusp_form.has_neg CuspForm.instNeg
 
 @[simp]
 theorem coe_neg (f : CuspForm Γ k) : ⇑(-f) = -f :=
@@ -358,9 +358,9 @@ theorem neg_apply (f : CuspForm Γ k) (z : ℍ) : (-f) z = -f z :=
   rfl
 #align cusp_form.neg_apply CuspForm.neg_apply
 
-instance hasSub : Sub (CuspForm Γ k) :=
+instance instSub : Sub (CuspForm Γ k) :=
   ⟨fun f g => f + -g⟩
-#align cusp_form.has_sub CuspForm.hasSub
+#align cusp_form.has_sub CuspForm.instSub
 
 @[simp]
 theorem coe_sub (f g : CuspForm Γ k) : ⇑(f - g) = f - g :=
@@ -375,7 +375,7 @@ theorem sub_apply (f g : CuspForm Γ k) (z : ℍ) : (f - g) z = f z - g z :=
 instance : AddCommGroup (CuspForm Γ k) :=
   FunLike.coe_injective.addCommGroup _ rfl coe_add coe_neg coe_sub coe_smul coe_smul
 
-/-- Additive coercion from `cusp_form` to `ℍ → ℂ`. -/
+/-- Additive coercion from `CuspForm` to `ℍ → ℂ`. -/
 @[simps]
 def coeHom : CuspForm Γ k →+ ℍ → ℂ where
   toFun f := f
diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
index a34b950f501a5..ecc6fd8be852d 100644
--- a/Mathlib/NumberTheory/NumberField/Units.lean
+++ b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -120,11 +120,11 @@ instance [NumberField K] : Finite (torsion K) := inferInstance
 instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _
 
 /-- The order of the torsion subgroup as positive integer. -/
-def torsion_order [NumberField K] : ℕ+ := ⟨Fintype.card (torsion K), Fintype.card_pos⟩
+def torsionOrder [NumberField K] : ℕ+ := ⟨Fintype.card (torsion K), Fintype.card_pos⟩
 
-/-- If `k` does not divide `torsion_order` then there are no nontrivial roots of unity of
+/-- If `k` does not divide `torsionOrder` then there are no nontrivial roots of unity of
   order dividing `k`. -/
-theorem rootsOfUnity_eq_one [NumberField K] {k : ℕ+} (hc : Nat.coprime k (torsion_order K)) :
+theorem rootsOfUnity_eq_one [NumberField K] {k : ℕ+} (hc : Nat.coprime k (torsionOrder K)) :
     ζ ∈ rootsOfUnity k (𝓞 K) ↔ ζ = 1 := by
   rw [mem_rootsOfUnity]
   refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
@@ -136,15 +136,15 @@ theorem rootsOfUnity_eq_one [NumberField K] {k : ℕ+} (hc : Nat.coprime k (tors
     rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
     exact orderOf_dvd_card_univ
 
-/-- The group of roots of unity of order dividing `torsion_order` is equal to the torsion
+/-- The group of roots of unity of order dividing `torsionOrder` is equal to the torsion
 group. -/
 theorem rootsOfUnity_eq_torsion [NumberField K] :
-    rootsOfUnity (torsion_order K) (𝓞 K) = torsion K := by
+    rootsOfUnity (torsionOrder K) (𝓞 K) = torsion K := by
   ext ζ
   rw [torsion, mem_rootsOfUnity]
   refine ⟨fun h => ?_, fun h => ?_⟩
   · rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
-    exact ⟨↑(torsion_order K), (torsion_order K).prop, h⟩
+    exact ⟨↑(torsionOrder K), (torsionOrder K).prop, h⟩
   · exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ ⟨ζ, h⟩ _)
 
 end torsion
diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
index fadbd33f99383..3dba8790462e5 100644
--- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean
+++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
@@ -50,7 +50,7 @@ open Function Order
 
 noncomputable section
 
-/-! ### Basic casts between `ordinal` and `nat_ordinal` -/
+/-! ### Basic casts between `Ordinal` and `NatOrdinal` -/
 
 /-- A type synonym for ordinals with natural addition and multiplication. -/
 def NatOrdinal : Type _ :=
diff --git a/Mathlib/Topology/PathConnected.lean b/Mathlib/Topology/PathConnected.lean
index a678b31171593..6eb5b7b8cb133 100644
--- a/Mathlib/Topology/PathConnected.lean
+++ b/Mathlib/Topology/PathConnected.lean
@@ -1156,7 +1156,7 @@ instance Quotient.instPathConnectedSpace {s : Setoid X} [PathConnectedSpace X] :
     PathConnectedSpace (Quotient s) :=
   (surjective_quotient_mk' X).pathConnectedSpace continuous_coinduced_rng
 
-/-- This is a special case of `NormedSpace.path_connected` (and
+/-- This is a special case of `NormedSpace.instPathConnectedSpace` (and
 `TopologicalAddGroup.pathConnectedSpace`). It exists only to simplify dependencies. -/
 instance Real.instPathConnectedSpace : PathConnectedSpace ℝ where
   Nonempty := inferInstance