chore: tidy various files (#3358)

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -12,7 +12,7 @@ import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.CategoryTheory.Endomorphism
 
 /-!
-# Category instances for group, add_group, comm_group, and add_comm_group.
+# Category instances for Group, AddGroup, CommGroup, and AddCommGroup.
 
 We introduce the bundled categories:
 * `GroupCat`
@@ -81,7 +81,7 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddGroup.of_hom AddGroupCat.ofHom
 
-/-- Typecheck a `add_monoid_hom` as a morphism in `AddGroup`. -/
+/-- Typecheck a `AddMonoidHom` as a morphism in `AddGroup`. -/
 add_decl_doc AddGroupCat.ofHom
 
 -- porting note: this instance was not necessary in mathlib
@@ -373,9 +373,10 @@ lemma Hom.map_mul {X Y : CommGroupCat} (f : X ⟶ Y) (x y : X) : f (x * y) = f x
 lemma Hom.map_one {X Y : CommGroupCat} (f : X ⟶ Y) : f (1 : X) = 1 := by
   apply MonoidHom.map_one (show MonoidHom X Y from f)
 
+-- Porting note: is this still relevant?
 -- This example verifies an improvement possible in Lean 3.8.
--- Before that, to have `monoid_hom.map_map` usable by `simp` here,
--- we had to mark all the concrete category `has_coe_to_sort` instances reducible.
+-- Before that, to have `MonoidHom.map_map` usable by `simp` here,
+-- we had to mark all the concrete category `CoeSort` instances reducible.
 -- Now, it just works.
 @[to_additive]
 example {R S : CommGroupCat} (i : R ⟶ S) (r : R) (h : r = 1) : i r = 1 := by simp [h]
@@ -386,7 +387,7 @@ namespace AddCommGroupCat
 
 -- Note that because `ℤ : Type 0`, this forces `G : AddCommGroup.{0}`,
 -- so we write this explicitly to be clear.
--- TODO generalize this, requiring a `ulift_instances.lean` file
+-- TODO generalize this, requiring a `ULiftInstances.lean` file
 /-- Any element of an abelian group gives a unique morphism from `ℤ` sending
 `1` to that element. -/
 def asHom {G : AddCommGroupCat.{0}} (g : G) : AddCommGroupCat.of ℤ ⟶ G :=
@@ -442,8 +443,7 @@ add_decl_doc AddEquiv.toAddGroupCatIso
 /-- Build an isomorphism in the category `CommGroupCat` from a `MulEquiv`
 between `CommGroup`s. -/
 @[to_additive (attr := simps)]
-def MulEquiv.toCommGroupCatIso {X Y : CommGroupCat} (e : X ≃* Y) : X ≅ Y
-    where
+def MulEquiv.toCommGroupCatIso {X Y : CommGroupCat} (e : X ≃* Y) : X ≅ Y where
   hom := CommGroupCat.Hom.mk e.toMonoidHom
   inv := CommGroupCat.Hom.mk e.symm.toMonoidHom
 set_option linter.uppercaseLean3 false in
@@ -501,8 +501,7 @@ add_decl_doc addEquivIsoAddGroupIso
 /-- multiplicative equivalences between `comm_group`s are the same as (isomorphic to) isomorphisms
 in `CommGroup` -/
 @[to_additive]
-def mulEquivIsoCommGroupIso {X Y : CommGroupCat.{u}} : X ≃* Y ≅ X ≅ Y
-    where
+def mulEquivIsoCommGroupIso {X Y : CommGroupCat.{u}} : X ≃* Y ≅ X ≅ Y where
   hom e := e.toCommGroupCatIso
   inv i := i.commGroupIsoToMulEquiv
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/GroupPower/Order.lean

@@ -156,7 +156,7 @@ theorem Right.pow_le_one_of_le (hx : x ≤ 1) : ∀ {n : ℕ}, x ^ n ≤ 1
 
 end Right
 
-section CovariantLtSwap
+section CovariantLTSwap
 
 variable [Preorder β] [CovariantClass M M (· * ·) (· < ·)]
   [CovariantClass M M (swap (· * ·)) (· < ·)] {f : β → M}
@@ -178,9 +178,9 @@ theorem pow_strictMono_right' {n : ℕ} (hn : n ≠ 0) : StrictMono fun a : M =>
 #align pow_strict_mono_right' pow_strictMono_right'
 #align nsmul_strict_mono_left nsmul_strictMono_left
 
-end CovariantLtSwap
+end CovariantLTSwap
 
-section CovariantLeSwap
+section CovariantLESwap
 
 variable [Preorder β] [CovariantClass M M (· * ·) (· ≤ ·)]
   [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
@@ -200,7 +200,7 @@ theorem pow_mono_right (n : ℕ) : Monotone fun a : M => a ^ n :=
 #align pow_mono_right pow_mono_right
 #align nsmul_mono_left nsmul_mono_left
 
-end CovariantLeSwap
+end CovariantLESwap
 
 @[to_additive Left.pow_neg]
 theorem Left.pow_lt_one_of_lt [CovariantClass M M (· * ·) (· < ·)] {n : ℕ} {x : M} (hn : 0 < n)
@@ -230,7 +230,7 @@ section LinearOrder
 
 variable [LinearOrder M]
 
-section CovariantLe
+section CovariantLE
 
 variable [CovariantClass M M (· * ·) (· ≤ ·)]
 
@@ -280,9 +280,9 @@ theorem pow_lt_pow_iff' (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
 #align pow_lt_pow_iff' pow_lt_pow_iff'
 #align nsmul_lt_nsmul_iff nsmul_lt_nsmul_iff
 
-end CovariantLe
+end CovariantLE
 
-section CovariantLeSwap
+section CovariantLESwap
 
 variable [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
 
@@ -314,9 +314,9 @@ theorem lt_max_of_sq_lt_mul {a b c : M} (h : a ^ 2 < b * c) : a < max b c := by
 #align lt_max_of_sq_lt_mul lt_max_of_sq_lt_mul
 #align lt_max_of_two_nsmul_lt_add lt_max_of_two_nsmul_lt_add
 
-end CovariantLeSwap
+end CovariantLESwap
 
-section CovariantLtSwap
+section CovariantLTSwap
 
 variable [CovariantClass M M (· * ·) (· < ·)] [CovariantClass M M (swap (· * ·)) (· < ·)]
 
@@ -338,7 +338,7 @@ theorem le_max_of_sq_le_mul {a b c : M} (h : a ^ 2 ≤ b * c) : a ≤ max b c :=
 #align le_max_of_sq_le_mul le_max_of_sq_le_mul
 #align le_max_of_two_nsmul_le_add le_max_of_two_nsmul_le_add
 
-end CovariantLtSwap
+end CovariantLTSwap
 
 @[to_additive Left.nsmul_neg_iff]
 theorem Left.pow_lt_one_iff' [CovariantClass M M (· * ·) (· < ·)] {n : ℕ} {x : M} (hn : 0 < n) :

Mathlib/CategoryTheory/Limits/Lattice.lean

@@ -140,7 +140,7 @@ instance (priority := 100) [SemilatticeSup α] [OrderBot α] : HasBinaryCoproduc
     infer_instance
   apply hasBinaryCoproducts_of_hasColimit_pair
 
-/-- The binary coproduct in the category of a `semilattice_sup` with `order_bot` is the same as the
+/-- The binary coproduct in the category of a `SemilatticeSup` with `OrderBot` is the same as the
 supremum.
 -/
 @[simp]
@@ -149,11 +149,11 @@ theorem coprod_eq_sup [SemilatticeSup α] [OrderBot α] (x y : α) : Limits.copr
     Limits.coprod x y = colimit (pair x y) := rfl
     _ = Finset.univ.sup (pair x y).obj := by rw [finite_colimit_eq_finset_univ_sup (pair x y)]
     _ = x ⊔ (y ⊔ ⊥) := rfl
-    -- Note: finset.sup is realized as a fold, hence the definitional equality
+    -- Note: Finset.sup is realized as a fold, hence the definitional equality
     _ = x ⊔ y := by rw [sup_bot_eq]
 #align category_theory.limits.complete_lattice.coprod_eq_sup CategoryTheory.Limits.CompleteLattice.coprod_eq_sup
 
-/-- The pullback in the category of a `semilattice_inf` with `order_top` is the same as the infimum
+/-- The pullback in the category of a `SemilatticeInf` with `OrderTop` is the same as the infimum
 over the objects.
 -/
 @[simp]
@@ -168,7 +168,7 @@ theorem pullback_eq_inf [SemilatticeInf α] [OrderTop α] {x y z : α} (f : x 
 
 #align category_theory.limits.complete_lattice.pullback_eq_inf CategoryTheory.Limits.CompleteLattice.pullback_eq_inf
 
-/-- The pushout in the category of a `semilattice_sup` with `order_bot` is the same as the supremum
+/-- The pushout in the category of a `SemilatticeSup` with `OrderBot` is the same as the supremum
 over the objects.
 -/
 @[simp]

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -459,7 +459,7 @@ noncomputable def ofPiFork (c : Fork I.fstPiMap I.sndPiMap) : Multifork I where
         rintro (_ | _) (_ | _) (_ | _ | _)
         · simp
         · simp
-        · dsimp ; rw [c.condition_assoc] ; simp
+        · dsimp; rw [c.condition_assoc]; simp
         · simp }
 #align category_theory.limits.multifork.of_pi_fork CategoryTheory.Limits.Multifork.ofPiFork
 
@@ -525,14 +525,11 @@ noncomputable def multiforkEquivPiFork : Multifork I ≌ Fork I.fstPiMap I.sndPi
           (by
             rintro (_ | _) <;> dsimp <;>
               simp [← Fork.app_one_eq_ι_comp_left, -Fork.app_one_eq_ι_comp_left]))
-      fun {K₁ K₂} f => by dsimp ; ext ; simp
+      fun {K₁ K₂} f => by dsimp; ext; simp
   counitIso :=
     NatIso.ofComponents
-      (fun K =>
-        Fork.ext (Iso.refl _)
-          (by dsimp ; ext ⟨j⟩ ; dsimp ; simp
-            ))
-      fun {K₁ K₂} f => by dsimp ; ext ; simp
+      (fun K => Fork.ext (Iso.refl _) (by dsimp; ext ⟨j⟩; dsimp; simp))
+      fun {K₁ K₂} f => by dsimp; ext; simp
 #align category_theory.limits.multicospan_index.multifork_equiv_pi_fork CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork
 
 end MulticospanIndex
@@ -690,8 +687,8 @@ variable (I : MultispanIndex C) [HasCoproduct I.left] [HasCoproduct I.right]
 @[simps]
 noncomputable def toSigmaCoforkFunctor : Multicofork I ⥤ Cofork I.fstSigmaMap I.sndSigmaMap where
   obj := Multicofork.toSigmaCofork
-  map {K₁ K₂} f := {
-    Hom := f.Hom
+  map {K₁ K₂} f :=
+  { Hom := f.Hom
     w := by
       rintro (_|_)
       all_goals {
@@ -729,9 +726,9 @@ noncomputable def multicoforkEquivSigmaCofork :
   unitIso :=
     NatIso.ofComponents (fun K => Cocones.ext (Iso.refl _) (by
       rintro (_ | _)
-      { dsimp; simp }
+      · dsimp; simp
       -- porting note; `dsimp, simp` worked in mathlib3.
-      { dsimp [Multicofork.ofSigmaCofork]; simp } ))
+      · dsimp [Multicofork.ofSigmaCofork]; simp ))
       fun {K₁ K₂} f => by
         -- porting note: in mathlib3 `ext` works and I don't
         -- really understand why it doesn't work here

Mathlib/CategoryTheory/Localization/Opposite.lean

@@ -31,17 +31,15 @@ variable {C D : Type _} [Category C] [Category D] {L : C ⥤ D} {W : MorphismPro
 namespace Localization
 
 /-- If `L : C ⥤ D` satisfies the universal property of the localisation
-for `W : morphism_property C`, then `L.op` also does. -/
+for `W : MorphismProperty C`, then `L.op` also does. -/
 def StrictUniversalPropertyFixedTarget.op {E : Type _} [Category E]
     (h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ) :
-    StrictUniversalPropertyFixedTarget L.op W.op E
-    where
+    StrictUniversalPropertyFixedTarget L.op W.op E where
   inverts := h.inverts.op
   lift F hF := (h.lift F.rightOp hF.rightOp).leftOp
   fac F hF := by
     convert congr_arg Functor.leftOp (h.fac F.rightOp hF.rightOp)
-  uniq F₁ F₂ eq :=
-    by
+  uniq F₁ F₂ eq := by
     suffices F₁.rightOp = F₂.rightOp by
       rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
     have eq' := congr_arg Functor.rightOp eq

Mathlib/CategoryTheory/Shift/Basic.lean

@@ -401,10 +401,10 @@ abbrev shiftZero : X⟦(0 : A)⟧ ≅ X :=
   (shiftFunctorZero C A).app _
 #align category_theory.shift_zero CategoryTheory.shiftZero
 
-theorem shift_zero' : f⟦(0 : A)⟧' = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv := by
+theorem shiftZero' : f⟦(0 : A)⟧' = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv := by
   symm
   apply NatIso.naturality_2
-#align category_theory.shift_zero' CategoryTheory.shift_zero'
+#align category_theory.shift_zero' CategoryTheory.shiftZero'
 
 variable (C) {A}
 
@@ -603,17 +603,17 @@ theorem shiftComm_symm (i j : A) : (shiftComm X i j).symm = shiftComm X j i := b
 variable {X Y}
 
 /-- When shifts are indexed by an additive commutative monoid, then shifts commute. -/
-theorem shift_comm' (i j : A) :
+theorem shiftComm' (i j : A) :
     f⟦i⟧'⟦j⟧' = (shiftComm _ _ _).hom ≫ f⟦j⟧'⟦i⟧' ≫ (shiftComm _ _ _).hom := by
   erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]
   dsimp
   simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]
-#align category_theory.shift_comm' CategoryTheory.shift_comm'
+#align category_theory.shift_comm' CategoryTheory.shiftComm'
 
 @[reassoc]
 theorem shiftComm_hom_comp (i j : A) :
     (shiftComm X i j).hom ≫ f⟦j⟧'⟦i⟧' = f⟦i⟧'⟦j⟧' ≫ (shiftComm Y i j).hom := by
-  rw [shift_comm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
+  rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
 #align category_theory.shift_comm_hom_comp CategoryTheory.shiftComm_hom_comp
 
 lemma shiftFunctorZero_hom_app_shift (n : A) :

Mathlib/CategoryTheory/Sites/Pretopology.lean

@@ -20,7 +20,7 @@ satisfying certain closure conditions.
 We show that a pretopology generates a genuine Grothendieck topology, and every topology has
 a maximal pretopology which generates it.
 
-The pretopology associated to a topological space is defined in `spaces.lean`.
+The pretopology associated to a topological space is defined in `Spaces.lean`.
 
 ## Tags
 
@@ -80,7 +80,8 @@ instance : CoeFun (Pretopology C) fun _ => ∀ X : C, Set (Presieve X) :=
 
 variable {C}
 
-instance LE : LE (Pretopology C) where le K₁ K₂ := (K₁ : ∀ X : C, Set (Presieve X)) ≤ K₂
+instance LE : LE (Pretopology C) where
+  le K₁ K₂ := (K₁ : ∀ X : C, Set (Presieve X)) ≤ K₂
 
 theorem le_def {K₁ K₂ : Pretopology C} : K₁ ≤ K₂ ↔ (K₁ : ∀ X : C, Set (Presieve X)) ≤ K₂ :=
   Iff.rfl

Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

@@ -201,7 +201,7 @@ theorem extend_agrees {x : FamilyOfElements P R} (t : x.Compatible) {f : Y ⟶ X
   have h := (le_generate R Y hf).choose_spec
   unfold FamilyOfElements.sieveExtend
   rw [t h.choose (𝟙 _) _ hf _]
-  · simp;
+  · simp
   · rw [id_comp]
     exact h.choose_spec.choose_spec.2
 #align category_theory.presieve.extend_agrees CategoryTheory.Presieve.extend_agrees
@@ -845,7 +845,7 @@ def forkMap : P.obj (op X) ⟶ FirstObj P R :=
 
 /-!
 This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and
-the definition of `is_sheaf_for`.
+the definition of `IsSheafFor`.
 -/
 
 
@@ -1026,7 +1026,7 @@ structure SheafOfTypes (J : GrothendieckTopology C) : Type max u₁ v₁ (w + 1)
   val : Cᵒᵖ ⥤ Type w
   /-- the condition that the presheaf is a sheaf -/
   cond : Presieve.IsSheaf J val
-  set_option linter.uppercaseLean3 false in
+set_option linter.uppercaseLean3 false in
 #align category_theory.SheafOfTypes CategoryTheory.SheafOfTypes
 
 namespace SheafOfTypes
@@ -1038,7 +1038,7 @@ variable {J}
 structure Hom (X Y : SheafOfTypes J) where
   /-- a morphism between the underlying presheaves -/
   val : X.val ⟶ Y.val
-  set_option linter.uppercaseLean3 false in
+set_option linter.uppercaseLean3 false in
 #align category_theory.SheafOfTypes.hom CategoryTheory.SheafOfTypes.Hom
 
 @[simps]

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -337,7 +337,7 @@ theorem infᵢ_adj_of_nonempty [Nonempty ι] {f : ι → SimpleGraph V} :
   rw [infᵢ, infₛ_adj_of_nonempty (Set.range_nonempty _), Set.forall_range_iff]
 #align simple_graph.infi_adj_of_nonempty SimpleGraph.infᵢ_adj_of_nonempty
 
-/-- For graphs `G`, `H`, `G ≤ H` iff `∀ a b, G.adj a b → H.adj a b`. -/
+/-- For graphs `G`, `H`, `G ≤ H` iff `∀ a b, G.Adj a b → H.Adj a b`. -/
 instance distribLattice : DistribLattice (SimpleGraph V) :=
   { show DistribLattice (SimpleGraph V) from
       adj_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl with

Mathlib/Data/List/Intervals.lean

@@ -14,7 +14,7 @@ import Mathlib.Data.Bool.Basic
 /-!
 # Intervals in ℕ
 
-This file defines intervals of naturals. `list.Ico m n` is the list of integers greater than `m`
+This file defines intervals of naturals. `List.Ico m n` is the list of integers greater than `m`
 and strictly less than `n`.
 
 ## TODO

Mathlib/Data/Matrix/DualNumber.lean

@@ -31,8 +31,9 @@ def Matrix.dualNumberEquiv : Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Mat
   left_inv A := Matrix.ext fun i j => TrivSqZeroExt.ext rfl rfl
   right_inv d := TrivSqZeroExt.ext (Matrix.ext fun i j => rfl) (Matrix.ext fun i j => rfl)
   map_mul' A B := by
-    ext; dsimp [mul_apply]
-    · simp_rw [fst_sum, fst_mul]
+    ext
+    · dsimp [mul_apply]
+      simp_rw [fst_sum, fst_mul]
       rfl
     · simp_rw [snd_sum, snd_mul, smul_eq_mul, op_smul_eq_mul, Finset.sum_add_distrib]
       simp [mul_apply, snd_sum, snd_mul]

Mathlib/Data/Multiset/Pi.lean

@@ -144,7 +144,7 @@ theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
     ∀ f : ∀ a ∈ m, β a, f ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a := by
   intro f
   induction' m using Multiset.induction_on with a m ih
-  . have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
+  · have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
     simp only [this, pi_zero, mem_singleton, true_iff]
     intro _ h; exact (not_mem_zero _ h).elim
   simp_rw [pi_cons, mem_bind, mem_map, ih]