diff --git a/Mathlib/Algebra/Category/Mon/FilteredColimits.lean b/Mathlib/Algebra/Category/Mon/FilteredColimits.lean
index 022cd95ece4184..e49501664c02e2 100644
--- a/Mathlib/Algebra/Category/Mon/FilteredColimits.lean
+++ b/Mathlib/Algebra/Category/Mon/FilteredColimits.lean
@@ -37,15 +37,14 @@ open CategoryTheory
 
 open CategoryTheory.Limits
 
-open CategoryTheory.IsFiltered renaming max → max'
+open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 
--- avoid name collision with `_root_.max`.
 namespace MonCat.FilteredColimits
 
 section
 
--- We use parameters here, mainly so we can have the abbreviations `M` and `M.mk` below, without
--- passing around `F` all the time.
+-- Porting note: mathlib 3 used `parameters` here, mainly so we can have the abbreviations `M` and
+-- `M.mk` below, without passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] (F : J ⥤ MonCat.{max v u})
 
 /-- The colimit of `F ⋙ forget Mon` in the category of types.
@@ -114,13 +113,13 @@ set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_zero_eq AddMonCat.FilteredColimits.colimit_zero_eq
 
 /-- The "unlifted" version of multiplication in the colimit. To multiply two dependent pairs
-`⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂` (given by `is_filtered.max`)
+`⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂` (given by `IsFiltered.max`)
 and multiply them there.
 -/
 @[to_additive
       "The \"unlifted\" version of addition in the colimit. To add two dependent pairs
       `⟨j₁, x⟩` and `⟨j₂, y⟩`, we pass to a common successor of `j₁` and `j₂`
-      (given by `is_filtered.max`) and add them there."]
+      (given by `IsFiltered.max`) and add them there."]
 noncomputable def colimitMulAux (x y : Σ j, F.obj j) : M.{v, u} F :=
   M.mk F ⟨IsFiltered.max x.fst y.fst, F.map (IsFiltered.leftToMax x.1 y.1) x.2 *
     F.map (IsFiltered.rightToMax x.1 y.1) y.2⟩
@@ -183,8 +182,8 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_aux_eq_of_rel_right AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right
 
-/-- Multiplication in the colimit. See also `colimit_mul_aux`. -/
-@[to_additive "Addition in the colimit. See also `colimit_add_aux`."]
+/-- Multiplication in the colimit. See also `colimitMulAux`. -/
+@[to_additive "Addition in the colimit. See also `colimitAddAux`."]
 noncomputable instance colimitMul : Mul (M.{v, u} F) :=
 { mul := fun x y => by
     refine' Quot.lift₂ (colimitMulAux F) _ _ x y
@@ -237,7 +236,7 @@ noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
       cases' x with j x
       rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, 1⟩ ⟨j, x⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one,
         one_mul, F.map_id]
-      -- Porting note : `id_apply` does not work hear, but the two handsides are def-eq
+      -- Porting note : `id_apply` does not work here, but the two sides are def-eq
       rfl
     mul_one := fun x => by
       refine Quot.inductionOn x ?_
@@ -245,7 +244,7 @@ noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
       cases' x with j x
       rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, 1⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one,
         mul_one, F.map_id]
-      -- Porting note : `id_apply` does not work hear, but the two handsides are def-eq
+      -- Porting note : `id_apply` does not work here, but the two sides are def-eq
       rfl
     mul_assoc := fun x y z => by
       refine Quot.induction_on₃ x y z ?_
diff --git a/Mathlib/Algebra/Category/Ring/Limits.lean b/Mathlib/Algebra/Category/Ring/Limits.lean
index 210876e61a86ff..4433b7f115a0ad 100644
--- a/Mathlib/Algebra/Category/Ring/Limits.lean
+++ b/Mathlib/Algebra/Category/Ring/Limits.lean
@@ -49,7 +49,7 @@ instance semiringObj (F : J ⥤ SemiRingCatMax.{v, u}) (j) :
 set_option linter.uppercaseLean3 false in
 #align SemiRing.semiring_obj SemiRingCat.semiringObj
 
-/-- The flat sections of a functor into `SemiRing` form a subsemiring of all sections.
+/-- The flat sections of a functor into `SemiRingCat` form a subsemiring of all sections.
 -/
 def sectionsSubsemiring (F : J ⥤ SemiRingCatMax.{v, u}) : Subsemiring.{max v u} (∀ j, F.obj j) :=
   -- Porting note : if `f` and `g` were inlined, it does not compile
@@ -68,7 +68,7 @@ instance limitSemiring (F : J ⥤ SemiRingCatMax.{v, u}) :
 set_option linter.uppercaseLean3 false in
 #align SemiRing.limit_semiring SemiRingCat.limitSemiring
 
-/-- `limit.π (F ⋙ forget SemiRing) j` as a `ring_hom`. -/
+/-- `limit.π (F ⋙ forget SemiRingCat) j` as a `RingHom`. -/
 def limitπRingHom (F : J ⥤ SemiRingCatMax.{v, u}) (j) :
     (Types.limitCone.{v, u} (F ⋙ forget SemiRingCat)).pt →+* (F ⋙ forget SemiRingCat).obj j :=
   -- Porting note : if `f` and `g` were inlined, it does not compile
@@ -82,10 +82,10 @@ set_option linter.uppercaseLean3 false in
 
 namespace HasLimits
 
--- The next two definitions are used in the construction of `has_limits SemiRing`.
+-- The next two definitions are used in the construction of `HasLimits SemiRingCat`.
 -- After that, the limits should be constructed using the generic limits API,
--- e.g. `limit F`, `limit.cone F`, and `limit.is_limit F`.
-/-- Construction of a limit cone in `SemiRing`.
+-- e.g. `limit F`, `limit.cone F`, and `limit.isLimit F`.
+/-- Construction of a limit cone in `SemiRingCat`.
 (Internal use only; use the limits API.)
 -/
 def limitCone (F : J ⥤ SemiRingCatMax.{v, u}) : Cone F where
@@ -97,7 +97,7 @@ def limitCone (F : J ⥤ SemiRingCatMax.{v, u}) : Cone F where
 set_option linter.uppercaseLean3 false in
 #align SemiRing.has_limits.limit_cone SemiRingCat.HasLimits.limitCone
 
-/-- Witness that the limit cone in `SemiRing` is a limit cone.
+/-- Witness that the limit cone in `SemiRingCat` is a limit cone.
 (Internal use only; use the limits API.)
 -/
 def limitConeIsLimit (F : J ⥤ SemiRingCatMax.{v, u}) : IsLimit (limitCone F) := by
@@ -139,8 +139,8 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from semirings to additive commutative monoids preserves all limits.
 -/
 instance forget₂AddCommMonPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ SemiRingCat AddCommMonCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ SemiRingCat AddCommMonCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (forget₂AddCommMonPreservesLimitsAux F) }
@@ -164,8 +164,8 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from semirings to monoids preserves all limits.
 -/
 instance forget₂MonPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ SemiRingCat MonCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ SemiRingCat MonCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit F)
           (forget₂MonPreservesLimitsAux.{v, u} F) }
@@ -179,8 +179,9 @@ set_option linter.uppercaseLean3 false in
 
 /-- The forgetful functor from semirings to types preserves all limits.
 -/
-instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget SemiRingCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+instance forgetPreservesLimitsOfSize :
+    PreservesLimitsOfSize.{v, v} (forget SemiRingCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit F)
           (Types.limitConeIsLimit.{v, u} (F ⋙ forget _)) }
@@ -217,15 +218,15 @@ instance limitCommSemiring (F : J ⥤ CommSemiRingCatMax.{v, u}) :
 set_option linter.uppercaseLean3 false in
 #align CommSemiRing.limit_comm_semiring CommSemiRingCat.limitCommSemiring
 
-/-- We show that the forgetful functor `CommSemiRing ⥤ SemiRing` creates limits.
+/-- We show that the forgetful functor `CommSemiRingCat ⥤ SemiRingCat` creates limits.
 
-All we need to do is notice that the limit point has a `comm_semiring` instance available,
+All we need to do is notice that the limit point has a `CommSemiring` instance available,
 and then reuse the existing limit.
 -/
 instance (F : J ⥤ CommSemiRingCatMax.{v, u}) :
     CreatesLimit F (forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u}) :=
-  -- Porting note : `CommSemiRing ⥤ Type` reflecting isomorphism is needed to make Lean see that
-  -- `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism. `CommSemiRing ⥤ Type` reflecting
+  -- Porting note : `CommSemiRingCat ⥤ Type` reflecting isomorphism is needed to make Lean see that
+  -- `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism. `CommSemiRingCat ⥤ Type` reflecting
   -- isomorphism is added manually since Lean can't see it, but even with this addition Lean can not
   -- see `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism, so this instance is also added.
   letI : ReflectsIsomorphisms (forget CommSemiRingCatMax.{v, u}) :=
@@ -253,7 +254,7 @@ instance (F : J ⥤ CommSemiRingCatMax.{v, u}) :
             fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y⟩)
           fun s => rfl }
 
-/-- A choice of limit cone for a functor into `CommSemiRing`.
+/-- A choice of limit cone for a functor into `CommSemiRingCat`.
 (Generally, you'll just want to use `limit F`.)
 -/
 def limitCone (F : J ⥤ CommSemiRingCatMax.{v, u}) : Cone F :=
@@ -272,8 +273,7 @@ set_option linter.uppercaseLean3 false in
 /- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of rings has all limits. -/
 instance hasLimitsOfSize : HasLimitsOfSize.{v, v} CommSemiRingCatMax.{v, u} :=
-  {
-    has_limits_of_shape := fun _ _ =>
+  { has_limits_of_shape := fun _ _ =>
       { has_limit := fun F =>
           hasLimit_of_created F (forget₂ CommSemiRingCat SemiRingCatMax.{v, u}) } }
 set_option linter.uppercaseLean3 false in
@@ -287,8 +287,8 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from rings to semirings preserves all limits.
 -/
 instance forget₂SemiRingPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ CommSemiRingCat SemiRingCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ CommSemiRingCat SemiRingCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (SemiRingCat.HasLimits.limitConeIsLimit _) }
@@ -305,8 +305,8 @@ set_option linter.uppercaseLean3 false in
 types could have been computed instead as limits in the category of types.)
 -/
 instance forgetPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget CommSemiRingCatMax.{v, u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget CommSemiRingCatMax.{v, u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (Types.limitConeIsLimit.{v, u} _) }
@@ -321,7 +321,7 @@ set_option linter.uppercaseLean3 false in
 end CommSemiRingCat
 
 -- Porting note: typemax hack to fix universe complaints
-/-- An alias for `Ring.{max u v}`, to deal around unification issues. -/
+/-- An alias for `RingCat.{max u v}`, to deal around unification issues. -/
 @[nolint checkUnivs]
 abbrev RingCatMax.{u1, u2} := RingCat.{max u1 u2}
 
@@ -335,7 +335,7 @@ instance ringObj (F : J ⥤ RingCatMax.{v, u}) (j) : Ring ((F ⋙ forget RingCat
 set_option linter.uppercaseLean3 false in
 #align Ring.ring_obj RingCat.ringObj
 
-/-- The flat sections of a functor into `Ring` form a subring of all sections.
+/-- The flat sections of a functor into `RingCat` form a subring of all sections.
 -/
 def sectionsSubring (F : J ⥤ RingCatMax.{v, u}) : Subring.{max v u} (∀ j, F.obj j) :=
   letI f : J ⥤ AddGroupCat.{max v u} :=
@@ -354,13 +354,13 @@ instance limitRing (F : J ⥤ RingCatMax.{v, u}) :
 set_option linter.uppercaseLean3 false in
 #align Ring.limit_ring RingCat.limitRing
 
-/-- We show that the forgetful functor `CommRing ⥤ Ring` creates limits.
+/-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.
 
-All we need to do is notice that the limit point has a `ring` instance available,
+All we need to do is notice that the limit point has a `Ring` instance available,
 and then reuse the existing limit.
 -/
 instance (F : J ⥤ RingCatMax.{v, u}) :
-  CreatesLimit F (forget₂ RingCatMax.{v, u} SemiRingCatMax.{v, u}) :=
+    CreatesLimit F (forget₂ RingCatMax.{v, u} SemiRingCatMax.{v, u}) :=
   letI : ReflectsIsomorphisms (forget₂ RingCatMax SemiRingCatMax) :=
     CategoryTheory.reflectsIsomorphisms_forget₂ _ _
   letI c : Cone F :=
@@ -376,7 +376,7 @@ instance (F : J ⥤ RingCatMax.{v, u}) :
         IsLimit.ofFaithful (forget₂ RingCat SemiRingCat.{max v u})
           (by apply SemiRingCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }
 
-/-- A choice of limit cone for a functor into `Ring`.
+/-- A choice of limit cone for a functor into `RingCat`.
 (Generally, you'll just want to use `limit F`.)
 -/
 def limitCone (F : J ⥤ RingCatMax.{v, u}) : Cone F :=
@@ -409,8 +409,8 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from rings to semirings preserves all limits.
 -/
 instance forget₂SemiRingPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ RingCat SemiRingCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ RingCat SemiRingCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
       { preservesLimit := fun {F} =>
           preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
             (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _) }
@@ -435,8 +435,8 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from rings to additive commutative groups preserves all limits.
 -/
 instance forget₂AddCommGroupPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ RingCatMax.{v, u} AddCommGroupCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ RingCatMax.{v, u} AddCommGroupCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (forget₂AddCommGroupPreservesLimitsAux F) }
@@ -452,8 +452,8 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from rings to types preserves all limits. (That is, the underlying
 types could have been computed instead as limits in the category of types.)
 -/
-instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget RingCatMax.{v, u})
-    where preservesLimitsOfShape {_ _} :=
+instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget RingCatMax.{v, u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (Types.limitConeIsLimit.{v, u} _) }
@@ -468,7 +468,7 @@ set_option linter.uppercaseLean3 false in
 end RingCat
 
 -- Porting note: typemax hack to fix universe complaints
-/-- An alias for `CommRing.{max u v}`, to deal around unification issues. -/
+/-- An alias for `CommRingCat.{max u v}`, to deal around unification issues. -/
 @[nolint checkUnivs]
 abbrev CommRingCatMax.{u1, u2} := CommRingCat.{max u1 u2}
 
@@ -490,9 +490,9 @@ instance limitCommRing (F : J ⥤ CommRingCatMax.{v, u}) :
 set_option linter.uppercaseLean3 false in
 #align CommRing.limit_comm_ring CommRingCat.limitCommRing
 
-/-- We show that the forgetful functor `CommRing ⥤ Ring` creates limits.
+/-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.
 
-All we need to do is notice that the limit point has a `comm_ring` instance available,
+All we need to do is notice that the limit point has a `CommRing` instance available,
 and then reuse the existing limit.
 -/
 instance (F : J ⥤ CommRingCatMax.{v, u}) :
@@ -500,7 +500,7 @@ instance (F : J ⥤ CommRingCatMax.{v, u}) :
   /-
     A terse solution here would be
     ```
-    creates_limit_of_fully_faithful_of_iso (CommRing.of (limit (F ⋙ forget _))) (iso.refl _)
+    createsLimitOfFullyFaithfulOfIso (CommRingCat.of (limit (F ⋙ forget _))) (Iso.refl _)
     ```
     but it seems this would introduce additional identity morphisms in `limit.π`.
     -/
@@ -531,7 +531,7 @@ instance (F : J ⥤ CommRingCatMax.{v, u}) :
                 (F ⋙ forget₂ CommRingCatMax.{v, u} RingCatMax.{v, u})).lift
                 ((forget₂ _ RingCatMax.{v, u}).mapCone s)) fun _ => rfl }
 
-/-- A choice of limit cone for a functor into `CommRing`.
+/-- A choice of limit cone for a functor into `CommRingCat`.
 (Generally, you'll just want to use `limit F`.)
 -/
 def limitCone (F : J ⥤ CommRingCatMax.{v, u}) : Cone F :=
@@ -569,8 +569,8 @@ set_option linter.uppercaseLean3 false in
 (That is, the underlying rings could have been computed instead as limits in the category of rings.)
 -/
 instance forget₂RingPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ CommRingCat RingCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ CommRingCat RingCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone.{v, v} (limitConeIsLimit.{v, u} F)
           (RingCat.limitConeIsLimit.{v, u} _) }
@@ -595,8 +595,8 @@ set_option linter.uppercaseLean3 false in
 in the category of commutative semirings.)
 -/
 instance forget₂CommSemiRingPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ CommRingCat CommSemiRingCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+    PreservesLimitsOfSize.{v, v} (forget₂ CommRingCat CommSemiRingCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (forget₂CommSemiRingPreservesLimitsAux.{v, u} F) }
@@ -612,8 +612,9 @@ set_option linter.uppercaseLean3 false in
 /-- The forgetful functor from commutative rings to types preserves all limits.
 (That is, the underlying types could have been computed instead as limits in the category of types.)
 -/
-instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget CommRingCat.{max v u})
-    where preservesLimitsOfShape {_ _} :=
+instance forgetPreservesLimitsOfSize :
+    PreservesLimitsOfSize.{v, v} (forget CommRingCat.{max v u}) where
+  preservesLimitsOfShape {_ _} :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone.{v, v} (limitConeIsLimit.{v, u} F)
           (Types.limitConeIsLimit.{v, u} _) }
diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean
index 6eb48b59742db1..52e5489b279d53 100644
--- a/Mathlib/Algebra/Free.lean
+++ b/Mathlib/Algebra/Free.lean
@@ -483,7 +483,7 @@ theorem mk_mul_mk (x y : α) (L1 L2 : List α) : mk x L1 * mk y L2 = mk x (L1 ++
 #align free_semigroup.mk_mul_mk FreeSemigroup.mk_mul_mk
 
 /-- The embedding `α → FreeSemigroup α`. -/
-@[to_additive (attr := simps) "The embedding `α → free_add_semigroup α`."]
+@[to_additive (attr := simps) "The embedding `α → FreeAddSemigroup α`."]
 def of (x : α) : FreeSemigroup α := ⟨x, []⟩
 #align free_semigroup.of FreeSemigroup.of
 
diff --git a/Mathlib/AlgebraicGeometry/PresheafedSpace.lean b/Mathlib/AlgebraicGeometry/PresheafedSpace.lean
index 9cf69541e9acc3..b968ddadc06dce 100644
--- a/Mathlib/AlgebraicGeometry/PresheafedSpace.lean
+++ b/Mathlib/AlgebraicGeometry/PresheafedSpace.lean
@@ -72,9 +72,9 @@ instance : CoeSort (PresheafedSpace C) (Type _) where coe := fun X => X.carrier
 -- porting note: the following lemma is removed because it is a syntactic tauto
 /-@[simp]
 theorem as_coe (X : PresheafedSpace.{w, v, u} C) : X.carrier = (X : TopCat.{w}) :=
-  rfl
+  rfl-/
 set_option linter.uppercaseLean3 false in
-#align algebraic_geometry.PresheafedSpace.as_coe AlgebraicGeometry.PresheafedSpace.as_coe-/
+#noalign algebraic_geometry.PresheafedSpace.as_coe
 
 -- porting note: removed @[simp] as the `simpVarHead` linter complains
 -- @[simp]
@@ -181,7 +181,7 @@ instance categoryOfPresheafedSpaces : Category (PresheafedSpace C) where
     . dsimp
       simp only [map_id, whiskerRight_id', assoc]
       erw [comp_id, comp_id]
-    . dsimp
+    · dsimp
       simp
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces
@@ -231,7 +231,7 @@ instance (X Y : PresheafedSpace C) : CoeFun (X ⟶ Y) fun _ => (↑X → ↑Y) :
 -- porting note: removed as this is a syntactic tauto
 --theorem coe_to_fun_eq {X Y : PresheafedSpace.{v, v, u} C} (f : X ⟶ Y) : (f : ↑X → ↑Y) = f.base :=
 --  rfl
---#align algebraic_geometry.PresheafedSpace.coe_to_fun_eq AlgebraicGeometry.PresheafedSpace.coe_to_fun_eq
+#noalign algebraic_geometry.PresheafedSpace.coe_to_fun_eq
 
 -- The `reassoc` attribute was added despite the LHS not being a composition of two homs,
 -- for the reasons explained in the docstring.
@@ -455,18 +455,18 @@ def restrictTopIso (X : PresheafedSpace C) : X.restrict (Opens.openEmbedding ⊤
   inv := X.toRestrictTop
   hom_inv_id := by
     ext
-    . dsimp
+    · dsimp
       erw [comp_c, toRestrictTop_c, whiskerRight_id',
         comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans, eqToHom_refl]
       rfl
-    . rfl
+    · rfl
   inv_hom_id := by
     ext
-    . dsimp
+    · dsimp
       erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
         eqToHom_trans, eqToHom_refl]
       rfl
-    . rfl
+    · rfl
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.restrict_top_iso AlgebraicGeometry.PresheafedSpace.restrictTopIso
 
diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
index b906ff7c8c90f5..88dbed257c51d7 100644
--- a/Mathlib/Data/Prod/Basic.lean
+++ b/Mathlib/Data/Prod/Basic.lean
@@ -113,9 +113,10 @@ theorem mk.inj_right {α β : Type _} (b : β) :
 #align prod.mk.inj_right Prod.mk.inj_right
 
 lemma mk_inj_left : (a, b₁) = (a, b₂) ↔ b₁ = b₂ := (mk.inj_left _).eq_iff
+#align prod.mk_inj_left Prod.mk_inj_left
+
 lemma mk_inj_right : (a₁, b) = (a₂, b) ↔ a₁ = a₂ := (mk.inj_right _).eq_iff
 #align prod.mk_inj_right Prod.mk_inj_right
-#align prod.mk_inj_left Prod.mk_inj_left
 
 theorem ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 := by
   rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index df29dd474fdbe1..6a38c2155c213b 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -1583,9 +1583,10 @@ lemma disjoint_union_right : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint
 #align set.disjoint_univ Set.disjoint_univ
 
 lemma disjoint_sdiff_left : Disjoint (t \ s) s := disjoint_sdiff_self_left
+#align set.disjoint_sdiff_left Set.disjoint_sdiff_left
+
 lemma disjoint_sdiff_right : Disjoint s (t \ s) := disjoint_sdiff_self_right
 #align set.disjoint_sdiff_right Set.disjoint_sdiff_right
-#align set.disjoint_sdiff_left Set.disjoint_sdiff_left
 
 theorem diff_union_diff_cancel (hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u :=
   sdiff_sup_sdiff_cancel hts hut
diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean
index 5a0c5b3b442a3e..93991f3d292a99 100644
--- a/Mathlib/GroupTheory/Perm/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Basic.lean
@@ -601,9 +601,10 @@ section AddGroup
 variable [AddGroup α] (a b : α)
 
 @[simp] lemma addLeft_zero : Equiv.addLeft (0 : α) = 1 := ext zero_add
+#align equiv.add_left_zero Equiv.addLeft_zero
+
 @[simp] lemma addRight_zero : Equiv.addRight (0 : α) = 1 := ext add_zero
 #align equiv.add_right_zero Equiv.addRight_zero
-#align equiv.add_left_zero Equiv.addLeft_zero
 
 @[simp] lemma addLeft_add : Equiv.addLeft (a + b) = Equiv.addLeft a * Equiv.addLeft b :=
   ext $ add_assoc _ _
@@ -614,9 +615,10 @@ variable [AddGroup α] (a b : α)
 #align equiv.add_right_add Equiv.addRight_add
 
 @[simp] lemma inv_addLeft : (Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a) := Equiv.coe_inj.1 rfl
+#align equiv.inv_add_left Equiv.inv_addLeft
+
 @[simp] lemma inv_addRight : (Equiv.addRight a)⁻¹ = Equiv.addRight (-a) := Equiv.coe_inj.1 rfl
 #align equiv.inv_add_right Equiv.inv_addRight
-#align equiv.inv_add_left Equiv.inv_addLeft
 
 @[simp] lemma pow_addLeft (n : ℕ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a) := by
   ext; simp [Perm.coe_pow]
@@ -642,10 +644,11 @@ variable [Group α] (a b : α)
 
 @[to_additive existing (attr := simp)]
 lemma mulLeft_one : Equiv.mulLeft (1 : α) = 1 := ext one_mul
+#align equiv.mul_left_one Equiv.mulLeft_one
+
 @[to_additive existing (attr := simp)]
 lemma mulRight_one : Equiv.mulRight (1 : α) = 1 := ext mul_one
 #align equiv.mul_right_one Equiv.mulRight_one
-#align equiv.mul_left_one Equiv.mulLeft_one
 
 @[to_additive existing (attr := simp)] lemma mulLeft_mul :
   Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b :=
@@ -659,10 +662,11 @@ ext $ fun _ ↦ (mul_assoc _ _ _).symm
 
 @[to_additive existing (attr := simp) inv_addLeft]
 lemma inv_mulLeft : (Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹ := Equiv.coe_inj.1 rfl
+#align equiv.inv_mul_left Equiv.inv_mulLeft
+
 @[to_additive existing (attr := simp) inv_addRight]
 lemma inv_mulRight : (Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹ := Equiv.coe_inj.1 rfl
 #align equiv.inv_mul_right Equiv.inv_mulRight
-#align equiv.inv_mul_left Equiv.inv_mulLeft
 
 @[to_additive existing (attr := simp) pow_addLeft]
 lemma pow_mulLeft (n : ℕ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) := by
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index b709658730ec55..5308cb82458b42 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -273,11 +273,13 @@ theorem Imp.swap : a → b → c ↔ b → a → c := ⟨Function.swap, Function
 #align imp.swap Imp.swap
 
 alias not_congr ← Iff.not
+#align iff.not Iff.not
+
 theorem Iff.not_left (h : a ↔ ¬b) : ¬a ↔ b := h.not.trans not_not
+#align iff.not_left Iff.not_left
+
 theorem Iff.not_right (h : ¬a ↔ b) : a ↔ ¬b := not_not.symm.trans h.not
 #align iff.not_right Iff.not_right
-#align iff.not_left Iff.not_left
-#align iff.not Iff.not
 
 /-! ### Declarations about `Xor'` -/
 
@@ -293,29 +295,33 @@ theorem xor_comm (a b) : Xor' a b = Xor' b a := by simp [Xor', and_comm, or_comm
 instance : IsCommutative Prop Xor' := ⟨xor_comm⟩
 
 @[simp] theorem xor_self (a : Prop) : Xor' a a = False := by simp [Xor']
+#align xor_self xor_self
+
 @[simp] theorem xor_not_left : Xor' (¬a) b ↔ (a ↔ b) := by by_cases a <;> simp [*]
+#align xor_not_left xor_not_left
+
 @[simp] theorem xor_not_right : Xor' a (¬b) ↔ (a ↔ b) := by by_cases a <;> simp [*]
+#align xor_not_right xor_not_right
+
 theorem xor_not_not : Xor' (¬a) (¬b) ↔ Xor' a b := by simp [Xor', or_comm, and_comm]
+#align xor_not_not xor_not_not
+
 protected theorem Xor'.or (h : Xor' a b) : a ∨ b := h.imp And.left And.left
 #align xor.or Xor'.or
-#align xor_not_not xor_not_not
-#align xor_not_right xor_not_right
-#align xor_not_left xor_not_left
-#align xor_self xor_self
 
 /-! ### Declarations about `and` -/
 
 alias and_congr ← Iff.and
+#align iff.and Iff.and
 #align and_congr_left and_congr_leftₓ -- reorder implicits
 #align and_congr_right' and_congr_right'ₓ -- reorder implicits
 #align and.right_comm and_right_comm
 #align and_and_distrib_left and_and_left
 #align and_and_distrib_right and_and_right
 alias and_rotate ↔ And.rotate _
+#align and.rotate And.rotate
 #align and.congr_right_iff and_congr_right_iff
 #align and.congr_left_iff and_congr_left_iffₓ -- reorder implicits
-#align and.rotate And.rotate
-#align iff.and Iff.and
 
 theorem and_symm_right (a b : α) (p : Prop) : p ∧ a = b ↔ p ∧ b = a := by simp [eq_comm]
 theorem and_symm_left (a b : α) (p : Prop) : a = b ∧ p ↔ b = a ∧ p := by simp [eq_comm]
@@ -323,12 +329,12 @@ theorem and_symm_left (a b : α) (p : Prop) : a = b ∧ p ↔ b = a ∧ p := by
 /-! ### Declarations about `or` -/
 
 alias or_congr ← Iff.or
+#align iff.or Iff.or
 #align or_congr_left' or_congr_left
 #align or_congr_right' or_congr_rightₓ -- reorder implicits
 #align or.right_comm or_right_comm
 alias or_rotate ↔ Or.rotate _
 #align or.rotate Or.rotate
-#align iff.or Iff.or
 
 @[deprecated Or.imp]
 theorem or_of_or_of_imp_of_imp (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → d) : c ∨ d := Or.imp h₂ h₃ h₁
@@ -477,11 +483,13 @@ theorem and_iff_not_or_not : a ∧ b ↔ ¬(¬a ∨ ¬b) := Decidable.and_iff_no
 #align not_xor not_xor
 
 theorem xor_iff_not_iff (P Q : Prop) : Xor' P Q ↔ ¬ (P ↔ Q) := (not_xor P Q).not_right
+#align xor_iff_not_iff xor_iff_not_iff
+
 theorem xor_iff_iff_not : Xor' a b ↔ (a ↔ ¬b) := by simp only [← @xor_not_right a, not_not]
+#align xor_iff_iff_not xor_iff_iff_not
+
 theorem xor_iff_not_iff' : Xor' a b ↔ (¬a ↔ b) := by simp only [← @xor_not_left _ b, not_not]
 #align xor_iff_not_iff' xor_iff_not_iff'
-#align xor_iff_iff_not xor_iff_iff_not
-#align xor_iff_not_iff xor_iff_not_iff
 
 end Propositional
 
@@ -1159,9 +1167,10 @@ theorem ite_eq_iff' : ite P a b = c ↔ (P → a = c) ∧ (¬P → b = c) := dit
 #align dite_eq_right_iff dite_eq_right_iff
 
 @[simp] theorem ite_eq_left_iff : ite P a b = a ↔ ¬P → b = a := dite_eq_left_iff
+#align ite_eq_left_iff ite_eq_left_iff
+
 @[simp] theorem ite_eq_right_iff : ite P a b = b ↔ P → a = b := dite_eq_right_iff
 #align ite_eq_right_iff ite_eq_right_iff
-#align ite_eq_left_iff ite_eq_left_iff
 
 theorem dite_ne_left_iff : dite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h := by
   rw [Ne.def, dite_eq_left_iff, not_forall]
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 49e26ad40b541c..9d02323c7e3f0f 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -603,14 +603,16 @@ theorem eq_update_iff {a : α} {b : β a} {f g : ∀ a, β a} :
 #align function.eq_update_iff Function.eq_update_iff
 
 @[simp] lemma update_eq_self_iff : update f a b = f ↔ b = f a := by simp [update_eq_iff]
+#align function.update_eq_self_iff Function.update_eq_self_iff
+
 @[simp] lemma eq_update_self_iff : f = update f a b ↔ f a = b := by simp [eq_update_iff]
 #align function.eq_update_self_iff Function.eq_update_self_iff
-#align function.update_eq_self_iff Function.update_eq_self_iff
 
 lemma ne_update_self_iff : f ≠ update f a b ↔ f a ≠ b := eq_update_self_iff.not
+#align function.ne_update_self_iff Function.ne_update_self_iff
+
 lemma update_ne_self_iff : update f a b ≠ f ↔ b ≠ f a := update_eq_self_iff.not
 #align function.update_ne_self_iff Function.update_ne_self_iff
-#align function.ne_update_self_iff Function.ne_update_self_iff
 
 @[simp]
 theorem update_eq_self (a : α) (f : ∀ a, β a) : update f a (f a) = f :=
@@ -990,7 +992,7 @@ def Set.piecewise {α : Type u} {β : α → Sort v} (s : Set α) (f g : ∀ i,
   fun i ↦ if i ∈ s then f i else g i
 #align set.piecewise Set.piecewise
 
-/-! ### Bijectivity of `eq.rec`, `eq.mp`, `eq.mpr`, and `cast` -/
+/-! ### Bijectivity of `Eq.rec`, `Eq.mp`, `Eq.mpr`, and `cast` -/
 
 
 theorem eq_rec_on_bijective {α : Sort _} {C : α → Sort _} :
diff --git a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
index 0d0372b99c17b8..003a231f234d87 100644
--- a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
+++ b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
@@ -510,11 +510,11 @@ theorem exists_normalized {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (las
     split_ifs with h; · exact h
     by_cases hi : ‖a.c i‖ = 0 <;> field_simp [norm_smul, hi]; norm_num
   refine' ⟨c', fun n => norm_c'_le n, fun i j inej => _⟩
-  -- up to exchanging `i` and `j`, one can assume `∥c i∥ ≤ ∥c j∥`.
+  -- up to exchanging `i` and `j`, one can assume `‖c i‖ ≤ ‖c j‖`.
   wlog hij : ‖a.c i‖ ≤ ‖a.c j‖ generalizing i j
   · rw [norm_sub_rev]; exact this j i inej.symm (le_of_not_le hij)
   rcases le_or_lt ‖a.c j‖ 2 with (Hj | Hj)
-  -- case `∥c j∥ ≤ 2` (and therefore also `∥c i∥ ≤ 2`)
+  -- case `‖c j‖ ≤ 2` (and therefore also `‖c i‖ ≤ 2`)
   · simp_rw [Hj, hij.trans Hj, if_true]
     exact exists_normalized_aux1 a lastr hτ δ hδ1 hδ2 i j inej
   -- case `2 < ‖c j‖`
diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean
index 8e4a2e113ca073..9c6598e3a0a11e 100644
--- a/Mathlib/Order/Lattice.lean
+++ b/Mathlib/Order/Lattice.lean
@@ -680,11 +680,11 @@ theorem sup_le_inf : a ⊔ b ≤ a ⊓ b ↔ a = b := by simp [le_antisymm_iff,
 #align sup_le_inf sup_le_inf
 
 @[simp] lemma inf_eq_sup : a ⊓ b = a ⊔ b ↔ a = b := by rw [←inf_le_sup.ge_iff_eq, sup_le_inf]
+#align inf_eq_sup inf_eq_sup
 @[simp] lemma sup_eq_inf : a ⊔ b = a ⊓ b ↔ a = b := eq_comm.trans inf_eq_sup
+#align sup_eq_inf sup_eq_inf
 @[simp] lemma inf_lt_sup : a ⊓ b < a ⊔ b ↔ a ≠ b := by rw [inf_le_sup.lt_iff_ne, Ne.def, inf_eq_sup]
 #align inf_lt_sup inf_lt_sup
-#align sup_eq_inf sup_eq_inf
-#align inf_eq_sup inf_eq_sup
 
 lemma inf_eq_and_sup_eq_iff : a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c := by
   refine' ⟨fun h ↦ _, _⟩
diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean
index 7c314b7e05775d..48cbc70e1e682c 100644
--- a/Mathlib/Tactic/ToAdditive.lean
+++ b/Mathlib/Tactic/ToAdditive.lean
@@ -106,7 +106,7 @@ namespace ToAdditive
 initialize registerTraceClass `to_additive
 initialize registerTraceClass `to_additive_detail
 
-/-- Linter to check that the reorder attribute is not given manually -/
+/-- Linter to check that the `reorder` attribute is not given manually -/
 register_option linter.toAdditiveReorder : Bool := {
   defValue := true
   descr := "Linter to check that the reorder attribute is not given manually." }
@@ -118,7 +118,7 @@ register_option linter.existingAttributeWarning : Bool := {
   descr := "Linter, mostly used by `@[to_additive]`, that checks that the source declaration " ++
     "doesn't have certain attributes" }
 
-/-- Linter to check that the reorder attribute is not given manually -/
+/-- Linter to check that the `to_additive` attribute is not given manually -/
 register_option linter.toAdditiveGenerateName : Bool := {
   defValue := true
   descr := "Linter used by `@[to_additive]` that checks if `@[to_additive]` automatically " ++
diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean
index 6662fc0a8398fd..de72fae862e07f 100644
--- a/Mathlib/Topology/Order/Basic.lean
+++ b/Mathlib/Topology/Order/Basic.lean
@@ -245,7 +245,7 @@ theorem IsClosed.hypograph [TopologicalSpace β] {f : β → α} {s : Set β} (h
   (hs.preimage continuous_fst).isClosed_le continuousOn_snd (hf.comp continuousOn_fst Subset.rfl)
 #align is_closed.hypograph IsClosed.hypograph
 
--- todo: move these lemmas to `Topology.Algebra.Order.LeftRight`
+-- Porting note: todo: move these lemmas to `Topology.Algebra.Order.LeftRight`
 theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) :=
   nhdsWithin_neBot_of_mem H₂
 #align nhds_within_Ici_ne_bot nhdsWithin_Ici_neBot
@@ -1250,7 +1250,7 @@ theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici {a : α} {s : Set α} (hs :
   rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
   · use a
     simpa [ha.Ici_eq] using hs
-  · rcases(nhdsWithin_Ici_basis' ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
+  · rcases (nhdsWithin_Ici_basis' ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
     rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hac, hcb⟩)
     · have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
       exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsWithin_Ici' hab, hbs⟩⟩
@@ -1959,7 +1959,7 @@ theorem IsLUB.frequently_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.None
     ∃ᶠ x in 𝓝[≤] a, x ∈ s := by
   rcases hs with ⟨a', ha'⟩
   intro h
-  rcases(ha.1 ha').eq_or_lt with (rfl | ha'a)
+  rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)
   · exact h.self_of_nhdsWithin le_rfl ha'
   · rcases (mem_nhdsWithin_Iic_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩
     rcases ha.exists_between hba with ⟨b', hb's, hb'⟩
@@ -2131,7 +2131,7 @@ theorem exists_seq_strictMono_tendsto' {α : Type _} [LinearOrder α] [Topologic
     ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x) := by
   have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
   have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
-  rcases(isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_not_mem hx ht with ⟨u, hu⟩
+  rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_not_mem hx ht with ⟨u, hu⟩
   exact ⟨u, hu.1, hu.2.2.symm⟩
 #align exists_seq_strict_mono_tendsto' exists_seq_strictMono_tendsto'
 
@@ -2152,7 +2152,7 @@ theorem exists_seq_strictMono_tendsto_nhdsWithin [DenselyOrdered α] [NoMinOrder
 theorem exists_seq_tendsto_sSup {α : Type _} [ConditionallyCompleteLinearOrder α]
     [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty)
     (hS' : BddAbove S) : ∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ n, u n ∈ S := by
-  rcases(isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
+  rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
   exact ⟨u, hu.1, hu.2.2⟩
 #align exists_seq_tendsto_Sup exists_seq_tendsto_sSup
 
@@ -2392,8 +2392,7 @@ theorem nhdsWithin_Ioi_self_neBot' {a : α} (H : (Ioi a).Nonempty) : NeBot (𝓝
   nhdsWithin_Ioi_neBot' H (le_refl a)
 #align nhds_within_Ioi_self_ne_bot' nhdsWithin_Ioi_self_neBot'
 
-@[instance]
-theorem nhdsWithin_Ioi_self_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) :=
+instance nhdsWithin_Ioi_self_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) :=
   nhdsWithin_Ioi_neBot (le_refl a)
 #align nhds_within_Ioi_self_ne_bot nhdsWithin_Ioi_self_neBot
 
@@ -2416,8 +2415,7 @@ theorem nhdsWithin_Iio_self_neBot' {b : α} (H : (Iio b).Nonempty) : NeBot (𝓝
   nhdsWithin_Iio_neBot' H (le_refl b)
 #align nhds_within_Iio_self_ne_bot' nhdsWithin_Iio_self_neBot'
 
-@[instance]
-theorem nhdsWithin_Iio_self_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) :=
+instance nhdsWithin_Iio_self_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) :=
   nhdsWithin_Iio_neBot (le_refl a)
 #align nhds_within_Iio_self_ne_bot nhdsWithin_Iio_self_neBot
 
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 33dd5b3e4e5a14..7e7cfa1c06b98a 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -716,9 +716,9 @@ theorem Dense.diff_singleton [T1Space α] {s : Set α} (hs : Dense s) (x : α) [
 obtains a dense set. -/
 theorem Dense.diff_finset [T1Space α] [∀ x : α, NeBot (𝓝[≠] x)] {s : Set α} (hs : Dense s)
     (t : Finset α) : Dense (s \ t) := by
-  induction t using Finset.induction_on -- with x s _ ih hd
-  case empty =>  simpa using hs
-  case insert ih =>
+  induction t using Finset.induction_on with
+  | empty =>  simpa using hs
+  | insert _ ih =>
     rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
     exact ih.diff_singleton _
 #align dense.diff_finset Dense.diff_finset
@@ -754,8 +754,8 @@ theorem ContinuousAt.eventually_ne [TopologicalSpace β] [T1Space β] {g : α 
 /-- To prove a function to a `T1Space` is continuous at some point `a`, it suffices to prove that
 `f` admits *some* limit at `a`. -/
 theorem continuousAt_of_tendsto_nhds [TopologicalSpace β] [T1Space β] {f : α → β} {a : α} {b : β}
-    (h : Tendsto f (𝓝 a) (𝓝 b)) : ContinuousAt f a :=
-  show Tendsto f (𝓝 a) (𝓝 <| f a) by rwa [eq_of_tendsto_nhds h]
+    (h : Tendsto f (𝓝 a) (𝓝 b)) : ContinuousAt f a := by
+  rwa [ContinuousAt, eq_of_tendsto_nhds h]
 #align continuous_at_of_tendsto_nhds continuousAt_of_tendsto_nhds
 
 @[simp]
@@ -1279,7 +1279,7 @@ theorem Bornology.relativelyCompact_eq_inCompact [T2Space α] :
 #align bornology.relatively_compact_eq_in_compact Bornology.relativelyCompact_eq_inCompact
 
 /-- If `V : ι → Set α` is a decreasing family of compact sets then any neighborhood of
-`⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhd_of_compact'` where we
+`⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
 don't need to assume each `V i` closed because it follows from compactness since `α` is
 assumed to be Hausdorff. -/
 theorem exists_subset_nhds_of_isCompact [T2Space α] {ι : Type _} [Nonempty ι] {V : ι → Set α}