From 6fff7165618b988f9172f1fa49ea20f40dba6df1 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sat, 18 Feb 2023 21:13:20 +0000
Subject: [PATCH] chore: tidy various files (#2321)

---
 Mathlib/Algebra/GradedMonoid.lean             |  82 +++++++-------
 Mathlib/CategoryTheory/Category/Preorder.lean |  37 +++---
 Mathlib/CategoryTheory/Equivalence.lean       |  19 ++--
 Mathlib/CategoryTheory/Pi/Basic.lean          | 106 ++++++++----------
 Mathlib/Combinatorics/Pigeonhole.lean         |  19 +---
 Mathlib/Data/Analysis/Filter.lean             |   6 +-
 Mathlib/Data/Dfinsupp/Lex.lean                |  12 +-
 Mathlib/GroupTheory/Finiteness.lean           |  28 ++---
 Mathlib/GroupTheory/Submonoid/Inverses.lean   |  14 +--
 Mathlib/Topology/Order.lean                   |   8 +-
 10 files changed, 154 insertions(+), 177 deletions(-)

diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean
index c63df6bb1fd08..da31aa29895f2 100644
--- a/Mathlib/Algebra/GradedMonoid.lean
+++ b/Mathlib/Algebra/GradedMonoid.lean
@@ -104,7 +104,7 @@ def GradedMonoid (A : ι → Type _) :=
 
 namespace GradedMonoid
 
-instance {A : ι → Type _} [Inhabited ι] [Inhabited (A default)] : Inhabited (GradedMonoid A) where 
+instance {A : ι → Type _} [Inhabited ι] [Inhabited (A default)] : Inhabited (GradedMonoid A) where
   default := Sigma.instInhabitedSigma.default
 
 /-- Construct an element of a graded monoid. -/
@@ -194,7 +194,7 @@ class GMonoid [AddMonoid ι] extends GMul A, GOne A where
   /-- Successor powers behave as expected -/
   gnpow_succ' :
     ∀ (n : ℕ) (a : GradedMonoid A),
-      (GradedMonoid.mk _ <| gnpow n.succ a.snd) = a * ⟨_, gnpow n a.snd⟩ := by 
+      (GradedMonoid.mk _ <| gnpow n.succ a.snd) = a * ⟨_, gnpow n a.snd⟩ := by
     apply_gmonoid_gnpowRec_succ_tac
 #align graded_monoid.gmonoid GradedMonoid.GMonoid
 
@@ -214,11 +214,11 @@ instance GMonoid.toMonoid [AddMonoid ι] [GMonoid A] : Monoid (GradedMonoid A)
 theorem mk_pow [AddMonoid ι] [GMonoid A] {i} (a : A i) (n : ℕ) :
     mk i a ^ n = mk (n • i) (GMonoid.gnpow _ a) :=
   by
-  match n with 
-  | 0 => 
+  match n with
+  | 0 =>
     rw [pow_zero]
     exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
-  | n+1 => 
+  | n+1 =>
     rw [pow_succ, mk_pow a n, mk_mul_mk]
     exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm
 #align graded_monoid.mk_pow GradedMonoid.mk_pow
@@ -268,7 +268,7 @@ variable [AddZeroClass ι] [GMul A]
 an `Eq.rec` to turn `A (0 + i)` into `A i`.
 -/
 instance GradeZero.smul (i : ι) : SMul (A 0) (A i)
-    where smul x y := @Eq.rec ι (0+i) (fun a _ => A a) (GMul.mul x y) i (zero_add i)   
+    where smul x y := @Eq.rec ι (0+i) (fun a _ => A a) (GMul.mul x y) i (zero_add i)
 #align graded_monoid.grade_zero.has_smul GradedMonoid.GradeZero.smul
 
 /-- `(*) : A 0 → A 0 → A 0` is the value provided in `GradedMonoid.GMul.mul`, composed with
@@ -281,7 +281,7 @@ variable {A}
 
 @[simp]
 theorem mk_zero_smul {i} (a : A 0) (b : A i) : mk _ (a • b) = mk _ a * mk _ b :=
-  Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ 
+  Sigma.ext (zero_add _).symm <| eq_rec_heq _ _
 #align graded_monoid.mk_zero_smul GradedMonoid.mk_zero_smul
 
 @[simp]
@@ -295,7 +295,7 @@ section Monoid
 
 variable [AddMonoid ι] [GMonoid A]
 
-instance : Pow (A 0) ℕ where 
+instance : Pow (A 0) ℕ where
   pow x n := @Eq.rec ι (n • (0:ι)) (fun a _ => A a) (GMonoid.gnpow n x) 0 (nsmul_zero n)
 
 variable {A}
@@ -376,9 +376,9 @@ theorem List.dProdIndex_cons (a : α) (l : List α) (fι : α → ι) :
 
 theorem List.dProdIndex_eq_map_sum (l : List α) (fι : α → ι) : l.dProdIndex fι = (l.map fι).sum :=
   by
-  match l with 
-  | [] => simp 
-  | head::tail => simp [List.dProdIndex_eq_map_sum tail fι] 
+  match l with
+  | [] => simp
+  | head::tail => simp [List.dProdIndex_eq_map_sum tail fι]
 #align list.dprod_index_eq_map_sum List.dProdIndex_eq_map_sum
 
 /-- A dependent product for graded monoids represented by the indexed family of types `A i`.
@@ -407,9 +407,9 @@ theorem List.dProd_cons (fι : α → ι) (fA : ∀ a, A (fι a)) (a : α) (l :
 theorem GradedMonoid.mk_list_dProd (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) :
     GradedMonoid.mk _ (l.dProd fι fA) = (l.map fun a => GradedMonoid.mk (fι a) (fA a)).prod :=
   by
-  match l with 
-  | [] => simp; rfl 
-  | head::tail => 
+  match l with
+  | [] => simp; rfl
+  | head::tail =>
     simp[← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
 #align graded_monoid.mk_list_dprod GradedMonoid.mk_list_dProd
 
@@ -450,7 +450,7 @@ structure. -/
 instance Monoid.gMonoid [AddMonoid ι] [Monoid R] : GradedMonoid.GMonoid fun _ : ι => R :=
   -- { Mul.gMul ι, One.gOne ι with
   { One.gOne ι with
-    mul := fun x y => x * y 
+    mul := fun x y => x * y
     one_mul := fun _ => Sigma.ext (zero_add _) (heq_of_eq (one_mul _))
     mul_one := fun _ => Sigma.ext (add_zero _) (heq_of_eq (mul_one _))
     mul_assoc := fun _ _ _ => Sigma.ext (add_assoc _ _ _) (heq_of_eq (mul_assoc _ _ _))
@@ -473,11 +473,11 @@ instance CommMonoid.gCommMonoid [AddCommMonoid ι] [CommMonoid R] :
 theorem List.dProd_monoid {α} [AddMonoid ι] [Monoid R] (l : List α) (fι : α → ι) (fA : α → R) :
     @List.dProd _ _ (fun _:ι => R) _ _ l fι fA = (l.map fA).prod  :=
   by
-  match l with 
-  | [] => 
+  match l with
+  | [] =>
     rw [List.dProd_nil, List.map_nil, List.prod_nil]
     rfl
-  | head::tail => 
+  | head::tail =>
     rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
     rfl
 #align list.dprod_monoid List.dProd_monoid
@@ -530,7 +530,7 @@ instance SetLike.gMul {S : Type _} [SetLike S R] [Mul R] [Add ι] (A : ι → S)
 #align set_like.ghas_mul SetLike.gMul
 
 /-
-Porting note: simpNF linter returns 
+Porting note: simpNF linter returns
 
 "Left-hand side does not simplify, when using the simp lemma on itself."
 
@@ -538,10 +538,10 @@ However, simp does indeed solve the following. Possibly related std#71,std#78
 
 example {S : Type _} [SetLike S R] [Mul R] [Add ι] (A : ι → S)
     [SetLike.GradedMul A] {i j : ι} (x : A i) (y : A j) :
-    ↑(@GradedMonoid.GMul.mul _ (fun i => A i) _ _ _ _ x y) = (x * y : R) := by simp 
+    ↑(@GradedMonoid.GMul.mul _ (fun i => A i) _ _ _ _ x y) = (x * y : R) := by simp
 
 -/
-@[simp,nolint simpNF] 
+@[simp,nolint simpNF]
 theorem SetLike.coe_gMul {S : Type _} [SetLike S R] [Mul R] [Add ι] (A : ι → S)
     [SetLike.GradedMul A] {i j : ι} (x : A i) (y : A j) :
     ↑(@GradedMonoid.GMul.mul _ (fun i => A i) _ _ _ _ x y) = (x * y : R) :=
@@ -562,11 +562,11 @@ variable {A : ι → S} [SetLike.GradedMonoid A]
 
 theorem pow_mem_graded (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i) :=
   by
-  match n with 
-  | 0 => 
+  match n with
+  | 0 =>
     rw [pow_zero, zero_nsmul]
     exact one_mem_graded _
-  | n+1 => 
+  | n+1 =>
     rw [pow_succ', succ_nsmul']
     exact mul_mem_graded (pow_mem_graded n h) h
 #align set_like.pow_mem_graded SetLike.pow_mem_graded
@@ -574,11 +574,11 @@ theorem pow_mem_graded (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A
 theorem list_prod_map_mem_graded {ι'} (l : List ι') (i : ι' → ι) (r : ι' → R)
     (h : ∀ j ∈ l, r j ∈ A (i j)) : (l.map r).prod ∈ A (l.map i).sum :=
   by
-  match l with 
-  | [] => 
+  match l with
+  | [] =>
     rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
     exact one_mem_graded _
-  | head::tail => 
+  | head::tail =>
     rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
     exact
       mul_mem_graded (h _ <| List.mem_cons_self _ _)
@@ -598,8 +598,7 @@ end SetLike
 instance SetLike.gMonoid {S : Type _} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S)
     [SetLike.GradedMonoid A] : GradedMonoid.GMonoid fun i => A i :=
   { SetLike.gOne A,
-    SetLike.gMul
-      A with
+    SetLike.gMul A with
     one_mul := fun ⟨_, _, _⟩ => Sigma.subtype_ext (zero_add _) (one_mul _)
     mul_one := fun ⟨_, _, _⟩ => Sigma.subtype_ext (add_zero _) (mul_one _)
     mul_assoc := fun ⟨_, _, _⟩ ⟨_, _, _⟩ ⟨_, _, _⟩ =>
@@ -610,7 +609,7 @@ instance SetLike.gMonoid {S : Type _} [SetLike S R] [Monoid R] [AddMonoid ι] (A
 #align set_like.gmonoid SetLike.gMonoid
 
 /-
-Porting note: simpNF linter returns 
+Porting note: simpNF linter returns
 
 "Left-hand side does not simplify, when using the simp lemma on itself."
 
@@ -621,7 +620,7 @@ example {S : Type _} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S)
     ↑(@GradedMonoid.GMonoid.gnpow _ (fun i => A i) _ _ n _ x) = (x:R)^n := by simp
 
 -/
-@[simp,nolint simpNF] 
+@[simp,nolint simpNF]
 theorem SetLike.coe_gnpow {S : Type _} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S)
     [SetLike.GradedMonoid A] {i : ι} (x : A i) (n : ℕ) :
     ↑(@GradedMonoid.GMonoid.gnpow _ (fun i => A i) _ _ n _ x) = (x:R)^n :=
@@ -642,30 +641,30 @@ open SetLike SetLike.GradedMonoid
 variable {α S : Type _} [SetLike S R] [Monoid R] [AddMonoid ι]
 
 /-
-Porting note: simpNF linter returns 
+Porting note: simpNF linter returns
 
 "Left-hand side does not simplify, when using the simp lemma on itself."
 
 However, simp does indeed solve the following. Possibly related std#71,std#78
 
 example (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι)
-    (fA : ∀ a, A (fι a)) (l : List α) : ↑(@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA) 
+    (fA : ∀ a, A (fι a)) (l : List α) : ↑(@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA)
     = (List.prod (l.map fun a => fA a) : R) := by simp
 -/
 /-- Coercing a dependent product of subtypes is the same as taking the regular product of the
 coercions. -/
-@[simp,nolint simpNF] 
+@[simp,nolint simpNF]
 theorem SetLike.coe_list_dProd (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι)
-    (fA : ∀ a, A (fι a)) (l : List α) : ↑(@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA) 
+    (fA : ∀ a, A (fι a)) (l : List α) : ↑(@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA)
     = (List.prod (l.map fun a => fA a) : R) := by
-  match l with 
-  | [] => 
+  match l with
+  | [] =>
     rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
-  | head::tail => 
-    rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons, 
+  | head::tail =>
+    rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
       SetLike.coe_list_dProd _ _ _ tail]
 #align set_like.coe_list_dprod SetLike.coe_list_dProd
- 
+
 /-- A version of `List.coe_dProd_set_like` with `Subtype.mk`. -/
 theorem SetLike.list_dProd_eq (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι) (fA : ∀ a, A (fι a))
     (l : List α) :
@@ -709,8 +708,7 @@ def SetLike.homogeneousSubmonoid [AddMonoid ι] [Monoid R] (A : ι → S) [SetLi
     Submonoid R where
   carrier := { a | SetLike.Homogeneous A a }
   one_mem' := SetLike.homogeneous_one A
-  mul_mem' a b := SetLike.homogeneous_mul a b 
+  mul_mem' a b := SetLike.homogeneous_mul a b
 #align set_like.homogeneous_submonoid SetLike.homogeneousSubmonoid
 
 end HomogeneousElements
-
diff --git a/Mathlib/CategoryTheory/Category/Preorder.lean b/Mathlib/CategoryTheory/Category/Preorder.lean
index 31a04a5eba656..afc484d1b5ba5 100644
--- a/Mathlib/CategoryTheory/Category/Preorder.lean
+++ b/Mathlib/CategoryTheory/Category/Preorder.lean
@@ -71,15 +71,15 @@ alias homOfLE ← _root_.LE.le.hom
 #align has_le.le.hom LE.le.hom
 
 @[simp]
-theorem hom_of_le_refl {x : X} : (le_refl x).hom = 𝟙 x :=
+theorem homOfLE_refl {x : X} : (le_refl x).hom = 𝟙 x :=
   rfl
-#align category_theory.hom_of_le_refl CategoryTheory.hom_of_le_refl
+#align category_theory.hom_of_le_refl CategoryTheory.homOfLE_refl
 
 @[simp]
-theorem hom_of_le_comp {x y z : X} (h : x ≤ y) (k : y ≤ z) :
+theorem homOfLE_comp {x y z : X} (h : x ≤ y) (k : y ≤ z) :
     homOfLE h ≫ homOfLE k = homOfLE (h.trans k) :=
   rfl
-#align category_theory.hom_of_le_comp CategoryTheory.hom_of_le_comp
+#align category_theory.hom_of_le_comp CategoryTheory.homOfLE_comp
 
 /-- Extract the underlying inequality from a morphism in a preorder category.
 -/
@@ -90,29 +90,28 @@ theorem leOfHom {x y : X} (h : x ⟶ y) : x ≤ y :=
 alias leOfHom ← _root_.Quiver.Hom.le
 #align quiver.hom.le Quiver.Hom.le
 
--- porting note: linter seems to be wrong here
-@[simp, nolint simpNF]
-theorem le_of_hom_hom_of_le {x y : X} (h : x ≤ y) : h.hom.le = h :=
+-- porting note: why does this lemma exist? With proof irrelevance, we don't need to simplify proofs
+-- @[simp]
+theorem leOfHom_homOfLE {x y : X} (h : x ≤ y) : h.hom.le = h :=
   rfl
-#align category_theory.le_of_hom_hom_of_le CategoryTheory.le_of_hom_hom_of_le
+#align category_theory.le_of_hom_hom_of_le CategoryTheory.leOfHom_homOfLE
 
--- porting note: linter gives: "Left-hand side does not simplify, when using the simp lemma on
--- itself. This usually means that it will never apply." removing simp? It doesn't fire
+-- porting note: why does this lemma exist? With proof irrelevance, we don't need to simplify proofs
 -- @[simp]
-theorem hom_of_le_le_of_hom {x y : X} (h : x ⟶ y) : h.le.hom = h := by
+theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h := by
   cases' h with h
   cases h
   rfl
-#align category_theory.hom_of_le_le_of_hom CategoryTheory.hom_of_le_le_of_hom
+#align category_theory.hom_of_le_le_of_hom CategoryTheory.homOfLE_leOfHom
 
 /-- Construct a morphism in the opposite of a preorder category from an inequality. -/
 def opHomOfLe {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x :=
   (homOfLE h).op
 #align category_theory.op_hom_of_le CategoryTheory.opHomOfLe
 
-theorem le_ofOp_hom {x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x :=
+theorem le_of_op_hom {x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x :=
   h.unop.le
-#align category_theory.le_of_op_hom CategoryTheory.le_ofOp_hom
+#align category_theory.le_of_op_hom CategoryTheory.le_of_op_hom
 
 instance uniqueToTop [OrderTop X] {x : X} : Unique (x ⟶ ⊤) where
   default := homOfLE le_top
@@ -132,10 +131,9 @@ variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y]
 
 /-- A monotone function between preorders induces a functor between the associated categories.
 -/
-def Monotone.functor {f : X → Y} (h : Monotone f) : X ⥤ Y
-    where
+def Monotone.functor {f : X → Y} (h : Monotone f) : X ⥤ Y where
   obj := f
-  map := @fun x₁ x₂ g => CategoryTheory.homOfLE (h g.le)
+  map g := CategoryTheory.homOfLE (h g.le)
 #align monotone.functor Monotone.functor
 
 @[simp]
@@ -169,13 +167,12 @@ theorem Iso.to_eq {x y : X} (f : x ≅ y) : x = y :=
 
 /-- A categorical equivalence between partial orders is just an order isomorphism.
 -/
-def Equivalence.toOrderIso (e : X ≌ Y) : X ≃o Y
-    where
+def Equivalence.toOrderIso (e : X ≌ Y) : X ≃o Y where
   toFun := e.functor.obj
   invFun := e.inverse.obj
   left_inv a := (e.unitIso.app a).to_eq.symm
   right_inv b := (e.counitIso.app b).to_eq
-  map_rel_iff' := @fun a a' =>
+  map_rel_iff' {a a'} :=
     ⟨fun h =>
       ((Equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (Equivalence.unitInv e).app a').le,
       fun h : a ≤ a' => (e.functor.map h.hom).le⟩
diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean
index dac17d3e0b1bc..e647b92d214c8 100644
--- a/Mathlib/CategoryTheory/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Equivalence.lean
@@ -697,9 +697,9 @@ namespace Equivalence
 
 See <https://stacks.math.columbia.edu/tag/02C3>.
 -/
-theorem ess_surj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F :=
+theorem essSurj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F :=
   ⟨fun Y => ⟨F.inv.obj Y, ⟨F.asEquivalence.counitIso.app Y⟩⟩⟩
-#align category_theory.equivalence.ess_surj_of_equivalence CategoryTheory.Equivalence.ess_surj_of_equivalence
+#align category_theory.equivalence.ess_surj_of_equivalence CategoryTheory.Equivalence.essSurj_of_equivalence
 
 -- see Note [lower instance priority]
 /-- An equivalence is faithful.
@@ -719,8 +719,8 @@ See <https://stacks.math.columbia.edu/tag/02C3>.
 -/
 instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Full F
     where
-  preimage := @fun X Y f => F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y
-  witness := @fun X Y f =>
+  preimage {X Y} f := F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y
+  witness {X Y} f :=
     F.inv.map_injective <| by
       simpa only [IsEquivalence.inv_fun_map, assoc, Iso.inv_hom_id_app_assoc,
         Iso.inv_hom_id_app] using comp_id _
@@ -730,9 +730,9 @@ instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : F
 private noncomputable def equivalenceInverse (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] : D ⥤ C
     where
   obj X := F.objPreimage X
-  map := @fun X Y f => F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
+  map {X Y} f := F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
   map_id X := by apply F.map_injective; aesop_cat
-  map_comp := @fun X Y Z f g => by apply F.map_injective; simp
+  map_comp {X Y Z} f g := by apply F.map_injective; simp
 -- #align category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse
 /- Porting note: this is a private def in mathlib -/
 
@@ -745,7 +745,7 @@ noncomputable def ofFullyFaithfullyEssSurj (F : C ⥤ D) [Full F] [Faithful F] [
     IsEquivalence F :=
   IsEquivalence.mk (equivalenceInverse F)
     (NatIso.ofComponents (fun X => (F.preimageIso <| F.objObjPreimageIso <| F.obj X).symm)
-      @fun X Y f => by
+      fun f => by
       apply F.map_injective
       aesop_cat)
     (NatIso.ofComponents F.objObjPreimageIso (by aesop_cat))
@@ -763,9 +763,8 @@ theorem inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) :
   functor_map_inj_iff e.symm f g
 #align category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff
 
-instance essSurjInducedFunctor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e)
-    where mem_essImage Y :=
-      ⟨e.symm Y, by simpa using ⟨default⟩⟩
+instance essSurjInducedFunctor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e) where
+  mem_essImage Y := ⟨e.symm Y, by simpa using ⟨default⟩⟩
 #align category_theory.equivalence.ess_surj_induced_functor CategoryTheory.Equivalence.essSurjInducedFunctor
 
 noncomputable instance inducedFunctorOfEquiv {C' : Type _} (e : C' ≃ D) :
diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index 3a6af452aae6c..dcb2885c5cd47 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -29,8 +29,7 @@ variable {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [∀ i, Category.
 
 /-- `pi C` gives the cartesian product of an indexed family of categories.
 -/
-instance pi : Category.{max w₀ v₁} (∀ i, C i)
-    where
+instance pi : Category.{max w₀ v₁} (∀ i, C i) where
   Hom X Y := ∀ i, X i ⟶ Y i
   id X i := 𝟙 (X i)
   comp f g i := f i ≫ g i
@@ -71,18 +70,17 @@ section
 
 variable {J : Type w₁}
 
-/- Porting note: add this because Lean cannot see directly through the `∘` for 
+/- Porting note: add this because Lean cannot see directly through the `∘` for
 `Function.comp` -/
 
-instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by 
+instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by
   dsimp
-  infer_instance 
+  infer_instance
 
 /-- Pull back an `I`-indexed family of objects to an `J`-indexed family, along a function `J → I`.
 -/
 @[simps]
-def comap (h : J → I) : (∀ i, C i) ⥤  (∀ j, C (h j))
-    where
+def comap (h : J → I) : (∀ i, C i) ⥤  (∀ j, C (h j)) where
   obj f i := f (h i)
   map α i := α (h i)
 #align category_theory.pi.comap CategoryTheory.Pi.comap
@@ -93,13 +91,12 @@ variable (I)
 pulling back a grading along the identity function,
 and the identity functor. -/
 @[simps]
-def comapId : comap C (id : I → I) ≅ 𝟭 (∀ i, C i)
-    where
+def comapId : comap C (id : I → I) ≅ 𝟭 (∀ i, C i) where
   hom := { app := fun X => 𝟙 X, naturality := by simp only [comap]; aesop_cat}
   inv := { app := fun X => 𝟙 X }
 #align category_theory.pi.comap_id CategoryTheory.Pi.comapId
 
-example (g : J → I) : (j : J) → Category (C (g j)) := by infer_instance 
+example (g : J → I) : (j : J) → Category (C (g j)) := by infer_instance
 
 variable {I}
 
@@ -110,21 +107,20 @@ pulling back along two successive functions, and
 pulling back along their composition
 -/
 @[simps!]
-def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f)
-    where
-  hom := { 
-    app := fun X b => 𝟙 (X (g (f b))) 
+def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f) where
+  hom := {
+    app := fun X b => 𝟙 (X (g (f b)))
     naturality := fun X Y f' => by simp only [comap,Function.comp]; funext; simp
     }
-  inv := { 
+  inv := {
     app := fun X b => 𝟙 (X (g (f b)))
     naturality := fun X Y f' => by simp only [comap,Function.comp]; funext; simp
     }
-  hom_inv_id := by 
-    simp only [comap] 
-    ext Y 
+  hom_inv_id := by
+    simp only [comap]
+    ext Y
     simp [CategoryStruct.comp,CategoryStruct.id]
-  inv_hom_id := by 
+  inv_hom_id := by
     simp only [comap]
     ext X
     simp [CategoryStruct.comp,CategoryStruct.id]
@@ -143,51 +139,49 @@ section
 variable {J : Type w₀} {D : J → Type u₁} [∀ j, Category.{v₁} (D j)]
 
 /- Porting note: maybe mixing up universes -/
-set_option align.precheck false
-instance sumElimCategoryₓ : ∀ s : Sum I J, Category.{v₁} (Sum.elim C D s)
+instance sumElimCategory : ∀ s : Sum I J, Category.{v₁} (Sum.elim C D s)
   | Sum.inl i => by
     dsimp
     infer_instance
   | Sum.inr j => by
     dsimp
     infer_instance
-#align category_theory.pi.sum_elim_category CategoryTheory.Pi.sumElimCategoryₓ 
+#align category_theory.pi.sum_elim_category CategoryTheory.Pi.sumElimCategoryₓ
 
-/- Porting note: replaced `Sum.rec` with `match`'s per the error about 
-current state of code generation -/ 
+/- Porting note: replaced `Sum.rec` with `match`'s per the error about
+current state of code generation -/
 
 /-- The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects
 to obtain an `I ⊕ J`-indexed family of objects.
 -/
 @[simps]
-def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : Sum I J, Sum.elim C D s
-    where
+def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : Sum I J, Sum.elim C D s where
   obj X :=
-    { obj := fun Y s => 
-        match s with 
-        | .inl i => X i 
+    { obj := fun Y s =>
+        match s with
+        | .inl i => X i
         | .inr j => Y j
-      map := fun {Y} {Y'} f s => 
-        match s with 
-        | .inl i => 𝟙 (X i) 
+      map := fun {Y} {Y'} f s =>
+        match s with
+        | .inl i => 𝟙 (X i)
         | .inr j => f j
-      map_id := fun Y => by 
+      map_id := fun Y => by
           dsimp
           simp only [CategoryStruct.id]
-          funext s 
-          match s with 
-          | .inl i => simp 
-          | .inr j => simp 
+          funext s
+          match s with
+          | .inl i => simp
+          | .inr j => simp
       map_comp := fun {Y₁} {Y₂} {Y₃} f g => by funext s; cases s; repeat {simp} }
-  map {X} {X'} f := 
-    { app := fun Y s => 
-        match s with 
-        | .inl i => f i 
-        | .inr j => 𝟙 (Y j) 
+  map {X} {X'} f :=
+    { app := fun Y s =>
+        match s with
+        | .inl i => f i
+        | .inr j => 𝟙 (Y j)
       naturality := fun {Y} {Y'} g => by funext s; cases s; repeat {simp} }
-  map_id := fun X => by 
+  map_id := fun X => by
     ext Y; dsimp; simp only [CategoryStruct.id]; funext s; cases s; repeat {simp}
-  map_comp := fun f g => by 
+  map_comp := fun f g => by
     ext Y; dsimp; simp only [CategoryStruct.comp]; funext s; cases s; repeat {simp}
 #align category_theory.pi.sum CategoryTheory.Pi.sum
 
@@ -234,8 +228,7 @@ variable {D : I → Type u₁} [∀ i, Category.{v₁} (D i)] {A : Type u₁} [C
 /-- Assemble an `I`-indexed family of functors into a functor between the pi types.
 -/
 @[simps]
-def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i
-    where
+def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i where
   obj f i := (F i).obj (f i)
   map α i := (F i).map (α i)
 #align category_theory.functor.pi CategoryTheory.Functor.pi
@@ -243,8 +236,7 @@ def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i
 /-- Similar to `pi`, but all functors come from the same category `A`
 -/
 @[simps]
-def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i
-    where
+def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i where
   obj a i := (f i).obj a
   map h i := (f i).map h
 #align category_theory.functor.pi' CategoryTheory.Functor.pi'
@@ -264,15 +256,15 @@ end EqToHom
 -- how `Functor.pi` commutes with `Pi.eval` and `Pi.comap`.
 @[simp]
 theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙  Pi.eval C i = f i := by
-  apply Functor.ext 
-  intro _ _ _ 
-  · simp 
-  · intro _ 
-    rfl 
+  apply Functor.ext
+  intro _ _ _
+  · simp
+  · intro _
+    rfl
 #align category_theory.functor.pi'_eval CategoryTheory.Functor.pi'_eval
 
 /-- Two functors to a product category are equal iff they agree on every coordinate. -/
-theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙  (Pi.eval C i) = f' ⋙  (Pi.eval C i)) 
+theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i))
     : f = f' := by
   apply Functor.ext; rotate_left
   · intro X
@@ -281,7 +273,7 @@ theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙  (Pi.eval C i) = f' 
     have := congr_obj h X
     simpa
   · intro X Y g
-    dsimp 
+    dsimp
     funext i
     specialize h i
     have := congr_hom h g
@@ -301,8 +293,8 @@ variable {F G : ∀ i, C i ⥤ D i}
 /-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
 -/
 @[simps!]
-def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where 
-  app f i := (α i).app (f i) 
+def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where
+  app f i := (α i).app (f i)
   naturality := fun X Y f => by simp [Functor.pi,CategoryStruct.comp]
 #align category_theory.nat_trans.pi CategoryTheory.NatTrans.pi
 
diff --git a/Mathlib/Combinatorics/Pigeonhole.lean b/Mathlib/Combinatorics/Pigeonhole.lean
index beba345524ce6..fa36d06434055 100644
--- a/Mathlib/Combinatorics/Pigeonhole.lean
+++ b/Mathlib/Combinatorics/Pigeonhole.lean
@@ -104,9 +104,6 @@ There are a few bits we can change in this theorem:
 We can do all these variations independently, so we have eight versions of the theorem.
 -/
 
--- porting note: several computations in the file seem to be timing out
-set_option maxHeartbeats 1000000
-
 section
 
 variable [LinearOrderedCancelAddCommMonoid M]
@@ -236,8 +233,7 @@ So, we prove four theorems: `Finset.exists_lt_card_fiber_of_maps_to_of_mul_lt_ca
 /-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
 at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes. -/
 theorem exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t)
-    (ht : t.card • b < s.card) : ∃ y ∈ t, b < (s.filter fun x => f x = y).card :=
-  by
+    (ht : t.card • b < s.card) : ∃ y ∈ t, b < (s.filter fun x => f x = y).card := by
   simp_rw [cast_card] at ht⊢
   exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht
 #align finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to
@@ -257,8 +253,7 @@ theorem exists_lt_card_fiber_of_mul_lt_card_of_maps_to (hf : ∀ a ∈ s, f a 
 /-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
 at most as many pigeons as the floor of the average number of pigeons across all pigeonholes. -/
 theorem exists_card_fiber_lt_of_card_lt_nsmul (ht : ↑s.card < t.card • b) :
-    ∃ y ∈ t, ↑(s.filter fun x => f x = y).card < b :=
-  by
+    ∃ y ∈ t, ↑(s.filter fun x => f x = y).card < b := by
   simp_rw [cast_card] at ht⊢
   exact
     exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
@@ -282,15 +277,14 @@ finite sets `s` and `t` and a number `b` such that `card t • b ≤ card s`, th
 that its preimage in `s` has at least `b` elements.
 See also `Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` for a stronger statement. -/
 theorem exists_le_card_fiber_of_nsmul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty)
-    (hb : t.card • b ≤ s.card) : ∃ y ∈ t, b ≤ (s.filter fun x => f x = y).card :=
-  by
+    (hb : t.card • b ≤ s.card) : ∃ y ∈ t, b ≤ (s.filter fun x => f x = y).card := by
   simp_rw [cast_card] at hb⊢
   exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb
 #align finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to
 
 /-- The pigeonhole principle for finitely many pigeons counted by heads: given a function between
-finite sets `s` and `t` and a natural number `b` such that `card t * n ≤ card s`, there exists `y ∈
-t` such that its preimage in `s` has at least `n` elements. See also
+finite sets `s` and `t` and a natural number `b` such that `card t * n ≤ card s`, there exists
+`y ∈ t` such that its preimage in `s` has at least `n` elements. See also
 `Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to` for a stronger statement. -/
 theorem exists_le_card_fiber_of_mul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty)
     (hn : t.card * n ≤ s.card) : ∃ y ∈ t, n ≤ (s.filter fun x => f x = y).card :=
@@ -302,8 +296,7 @@ finite sets `s` and `t`, and a number `b` such that `card s ≤ card t • b`, t
 that its preimage in `s` has no more than `b` elements.
 See also `Finset.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement. -/
 theorem exists_card_fiber_le_of_card_le_nsmul (ht : t.Nonempty) (hb : ↑s.card ≤ t.card • b) :
-    ∃ y ∈ t, ↑(s.filter fun x => f x = y).card ≤ b :=
-  by
+    ∃ y ∈ t, ↑(s.filter fun x => f x = y).card ≤ b := by
   simp_rw [cast_card] at hb⊢
   refine'
     exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
diff --git a/Mathlib/Data/Analysis/Filter.lean b/Mathlib/Data/Analysis/Filter.lean
index c58c9b74ccf60..71201c43e7a7f 100644
--- a/Mathlib/Data/Analysis/Filter.lean
+++ b/Mathlib/Data/Analysis/Filter.lean
@@ -318,16 +318,16 @@ protected def bind {f : Filter α} {m : α → Filter β} (F : f.Realizer) (G :
           ⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩⟩
 #align filter.realizer.bind Filter.Realizer.bind
 
--- Porting note: `Sup` had a long dubious translation message. I added `ₓ` to be safe.
+-- Porting note: `supᵢ` had a long dubious translation message. I added `ₓ` to be safe.
 /-- Construct a realizer for indexed supremum -/
-protected def Sup {f : α → Filter β} (F : ∀ i, (f i).Realizer) : (⨆ i, f i).Realizer :=
+protected def supᵢ {f : α → Filter β} (F : ∀ i, (f i).Realizer) : (⨆ i, f i).Realizer :=
   let F' : (⨆ i, f i).Realizer :=
     (Realizer.bind Realizer.top F).ofEq <|
       filter_eq <| Set.ext <| by simp [Filter.bind, eq_univ_iff_forall, supᵢ_sets_eq]
   F'.ofEquiv <|
     show (Σ_ : Unit, ∀ i : α, True → (F i).σ) ≃ ∀ i, (F i).σ from
       ⟨fun ⟨_, f⟩ i ↦ f i ⟨⟩, fun f ↦ ⟨(), fun i _ ↦ f i⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩
-#align filter.realizer.Sup Filter.Realizer.Supₓ
+#align filter.realizer.Sup Filter.Realizer.supᵢₓ
 
 /-- Construct a realizer for the product of filters -/
 protected def prod {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f.prod g).Realizer :=
diff --git a/Mathlib/Data/Dfinsupp/Lex.lean b/Mathlib/Data/Dfinsupp/Lex.lean
index 24857bc4f08a2..06b3dd258e0b2 100644
--- a/Mathlib/Data/Dfinsupp/Lex.lean
+++ b/Mathlib/Data/Dfinsupp/Lex.lean
@@ -102,16 +102,16 @@ private def lt_trichotomy_rec {P : Lex (Π₀ i, α i) → Lex (Π₀ i, α i) 
         not_mem_neLocus.mp (Finset.not_mem_of_lt_min hj <| by rwa [neLocus_comm]), hwit⟩
 
 /-- The less-or-equal relation for the lexicographic ordering is decidable. -/
-irreducible_def Lex.decidableLe : @DecidableRel (Lex (Π₀ i, α i)) (· ≤ ·) :=
+irreducible_def Lex.decidableLE : @DecidableRel (Lex (Π₀ i, α i)) (· ≤ ·) :=
   lt_trichotomy_rec (fun h ↦ isTrue <| Or.inr h)
     (fun h ↦ isTrue <| Or.inl <| congr_arg _ <| congr_arg _ h)
     fun h ↦ isFalse fun h' ↦ lt_irrefl _ (h.trans_le h')
-#align dfinsupp.lex.decidable_le Dfinsupp.Lex.decidableLe
+#align dfinsupp.lex.decidable_le Dfinsupp.Lex.decidableLE
 
 /-- The less-than relation for the lexicographic ordering is decidable. -/
-irreducible_def Lex.decidableLt : @DecidableRel (Lex (Π₀ i, α i)) (· < ·) :=
+irreducible_def Lex.decidableLT : @DecidableRel (Lex (Π₀ i, α i)) (· < ·) :=
   lt_trichotomy_rec (fun h ↦ isTrue h) (fun h ↦ isFalse h.not_lt) fun h ↦ isFalse h.asymm
-#align dfinsupp.lex.decidable_lt Dfinsupp.Lex.decidableLt
+#align dfinsupp.lex.decidable_lt Dfinsupp.Lex.decidableLT
 
 -- Porting note: Added `DecidableEq` for `LinearOrder`.
 instance : DecidableEq (Lex (Π₀ i, α i)) :=
@@ -122,8 +122,8 @@ instance : DecidableEq (Lex (Π₀ i, α i)) :=
 instance Lex.linearOrder : LinearOrder (Lex (Π₀ i, α i)) :=
   { Lex.partialOrder with
     le_total := lt_trichotomy_rec (fun h ↦ Or.inl h.le) (fun h ↦ Or.inl h.le) fun h ↦ Or.inr h.le
-    decidable_lt := decidableLt
-    decidable_le := decidableLe
+    decidable_lt := decidableLT
+    decidable_le := decidableLE
     decidable_eq := inferInstance }
 #align dfinsupp.lex.linear_order Dfinsupp.Lex.linearOrder
 
diff --git a/Mathlib/GroupTheory/Finiteness.lean b/Mathlib/GroupTheory/Finiteness.lean
index b8fda9527e127..91b2a3e961096 100644
--- a/Mathlib/GroupTheory/Finiteness.lean
+++ b/Mathlib/GroupTheory/Finiteness.lean
@@ -26,7 +26,7 @@ finitely-generated modules.
 * `Submonoid.Fg S`, `AddSubmonoid.Fg S` : A submonoid `S` is finitely generated.
 * `Monoid.Fg M`, `AddMonoid.Fg M` : A typeclass indicating a type `M` is finitely generated as a
 monoid.
-* `Subgroup.Fg S`, `AddSubgroup.fg S` : A subgroup `S` is finitely generated.
+* `Subgroup.Fg S`, `AddSubgroup.Fg S` : A subgroup `S` is finitely generated.
 * `Group.Fg M`, `AddGroup.Fg M` : A typeclass indicating a type `M` is finitely generated as a
 group.
 
@@ -54,7 +54,7 @@ def Submonoid.Fg (P : Submonoid M) : Prop :=
 add_decl_doc AddSubmonoid.Fg
 
 /-- An equivalent expression of `Submonoid.Fg` in terms of `Set.Finite` instead of `Finset`. -/
-@[to_additive "An equivalent expression of `AddSubmonoid.fg` in terms of `Set.Finite` instead of
+@[to_additive "An equivalent expression of `AddSubmonoid.Fg` in terms of `Set.Finite` instead of
 `Finset`."]
 theorem Submonoid.fg_iff (P : Submonoid M) :
     Submonoid.Fg P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite :=
@@ -109,7 +109,7 @@ theorem AddMonoid.fg_def : AddMonoid.Fg N ↔ (⊤ : AddSubmonoid N).Fg :=
 
 /-- An equivalent expression of `Monoid.Fg` in terms of `Set.Finite` instead of `Finset`. -/
 @[to_additive
-      "An equivalent expression of `AddMonoid.fg` in terms of `Set.Finite` instead of `Finset`."]
+      "An equivalent expression of `AddMonoid.Fg` in terms of `Set.Finite` instead of `Finset`."]
 theorem Monoid.fg_iff :
     Monoid.Fg M ↔ ∃ S : Set M, Submonoid.closure S = (⊤ : Submonoid M) ∧ S.Finite :=
   ⟨fun h => (Submonoid.fg_iff ⊤).1 h.out, fun h => ⟨(Submonoid.fg_iff ⊤).2 h⟩⟩
@@ -245,7 +245,7 @@ theorem Subgroup.fg_iff (P : Subgroup G) :
 #align add_subgroup.fg_iff AddSubgroup.fg_iff
 
 /-- A subgroup is finitely generated if and only if it is finitely generated as a submonoid. -/
-@[to_additive AddSubgroup.FgIffAddSubmonoid.fg "An additive subgroup is finitely generated if
+@[to_additive "An additive subgroup is finitely generated if
 and only if it is finitely generated as an additive submonoid."]
 theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.Fg ↔ P.toSubmonoid.Fg := by
   constructor
@@ -260,15 +260,15 @@ theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.Fg ↔ P.toSubmonoid.F
     · rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
       exact Subgroup.subset_closure
 #align subgroup.fg_iff_submonoid_fg Subgroup.fg_iff_submonoid_fg
-#align add_subgroup.fg_iff_add_submonoid.fg AddSubgroup.FgIffAddSubmonoid.fg
+#align add_subgroup.fg_iff_add_submonoid.fg AddSubgroup.fg_iff_addSubmonoid_fg
 
 theorem Subgroup.fg_iff_add_fg (P : Subgroup G) : P.Fg ↔ P.toAddSubgroup.Fg := by
-  rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.FgIffAddSubmonoid.fg]
+  rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
   exact (Subgroup.toSubmonoid P).fg_iff_add_fg
 #align subgroup.fg_iff_add_fg Subgroup.fg_iff_add_fg
 
 theorem AddSubgroup.fg_iff_mul_fg (P : AddSubgroup H) : P.Fg ↔ P.toSubgroup.Fg := by
-  rw [AddSubgroup.FgIffAddSubmonoid.fg, Subgroup.fg_iff_submonoid_fg]
+  rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
   exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)
 #align add_subgroup.fg_iff_mul_fg AddSubgroup.fg_iff_mul_fg
 
@@ -317,13 +317,13 @@ theorem Group.fg_iff' :
 #align add_group.fg_iff' AddGroup.fg_iff'
 
 /-- A group is finitely generated if and only if it is finitely generated as a monoid. -/
-@[to_additive AddGroup.FgIffAddMonoid.fg "An additive group is finitely generated if and only
+@[to_additive "An additive group is finitely generated if and only
 if it is finitely generated as an additive monoid."]
-theorem Group.FgIffMonoid.fg : Group.Fg G ↔ Monoid.Fg G :=
+theorem Group.fg_iff_monoid_fg : Group.Fg G ↔ Monoid.Fg G :=
   ⟨fun h => Monoid.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).1 (Group.fg_def.1 h), fun h =>
     Group.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).2 (Monoid.fg_def.1 h)⟩
-#align group.fg_iff_monoid.fg Group.FgIffMonoid.fg
-#align add_group.fg_iff_add_monoid.fg AddGroup.FgIffAddMonoid.fg
+#align group.fg_iff_monoid.fg Group.fg_iff_monoid_fg
+#align add_group.fg_iff_add_monoid.fg AddGroup.fg_iff_addMonoid_fg
 
 theorem GroupFg.iff_add_fg : Group.Fg G ↔ AddGroup.Fg (Additive G) :=
   ⟨fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).1 h.out⟩, fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).2 h.out⟩⟩
@@ -352,7 +352,8 @@ instance (priority := 100) Group.fg_of_finite [Finite G] : Group.Fg G := by
 @[to_additive]
 theorem Group.fg_of_surjective {G' : Type _} [Group G'] [hG : Group.Fg G] {f : G →* G'}
     (hf : Function.Surjective f) : Group.Fg G' :=
-  Group.FgIffMonoid.fg.mpr <| @Monoid.fg_of_surjective G _ G' _ (Group.FgIffMonoid.fg.mp hG) f hf
+  Group.fg_iff_monoid_fg.mpr <|
+    @Monoid.fg_of_surjective G _ G' _ (Group.fg_iff_monoid_fg.mp hG) f hf
 #align group.fg_of_surjective Group.fg_of_surjective
 #align add_group.fg_of_surjective AddGroup.fg_of_surjective
 
@@ -440,8 +441,7 @@ theorem rank_congr {H K : Subgroup G} [Group.Fg H] [Group.Fg K] (h : H = K) :
 theorem rank_closure_finset_le_card (s : Finset G) : Group.rank (closure (s : Set G)) ≤ s.card := by
   classical
     let t : Finset (closure (s : Set G)) := s.preimage Subtype.val (Subtype.coe_injective.injOn _)
-    have ht : closure (t : Set (closure (s : Set G))) = ⊤ :=
-      by
+    have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
       rw [Finset.coe_preimage]
       exact closure_preimage_eq_top (s : Set G)
     apply (Group.rank_le (closure (s : Set G)) ht).trans
diff --git a/Mathlib/GroupTheory/Submonoid/Inverses.lean b/Mathlib/GroupTheory/Submonoid/Inverses.lean
index 6a2f85277f8f4..37d62cc01b680 100644
--- a/Mathlib/GroupTheory/Submonoid/Inverses.lean
+++ b/Mathlib/GroupTheory/Submonoid/Inverses.lean
@@ -129,23 +129,22 @@ theorem fromLeftInv_mul (x : S.leftInv) : (S.fromLeftInv x : M) * x = 1 := by
 #align add_submonoid.from_left_neg_add AddSubmonoid.fromLeftNeg_add
 
 @[to_additive]
-theorem leftInv_le_is_unit : S.leftInv ≤ IsUnit.submonoid M := fun x ⟨y, hx⟩ ↦
+theorem leftInv_le_isUnit : S.leftInv ≤ IsUnit.submonoid M := fun x ⟨y, hx⟩ ↦
   ⟨⟨x, y, hx, mul_comm x y ▸ hx⟩, rfl⟩
-#align submonoid.left_inv_le_is_unit Submonoid.leftInv_le_is_unit
-#align add_submonoid.left_neg_le_is_add_unit AddSubmonoid.leftNeg_le_is_addUnit
+#align submonoid.left_inv_le_is_unit Submonoid.leftInv_le_isUnit
+#align add_submonoid.left_neg_le_is_add_unit AddSubmonoid.leftNeg_le_isAddUnit
 
 @[to_additive]
 theorem fromLeftInv_eq_iff (a : S.leftInv) (b : M) : (S.fromLeftInv a : M) = b ↔ (a : M) * b = 1 :=
-  by rw [← IsUnit.mul_right_inj (leftInv_le_is_unit _ a.prop), S.mul_fromLeftInv, eq_comm]
+  by rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]
 #align submonoid.from_left_inv_eq_iff Submonoid.fromLeftInv_eq_iff
 #align add_submonoid.from_left_neg_eq_iff AddSubmonoid.fromLeftNeg_eq_iff
 
 /-- The `MonoidHom` from `S.leftInv` to `S` sending an element to its right inverse in `S`. -/
 @[to_additive (attr := simps)
-    "The `add_monoid_hom` from `S.leftNeg` to `S` sending an element to its
+    "The `AddMonoidHom` from `S.leftNeg` to `S` sending an element to its
     right additive inverse in `S`."]
-noncomputable def fromCommLeftInv : S.leftInv →* S
-    where
+noncomputable def fromCommLeftInv : S.leftInv →* S where
   toFun := S.fromLeftInv
   map_one' := S.fromLeftInv_one
   map_mul' x y :=
@@ -198,7 +197,6 @@ theorem leftInvEquiv_symm_fromLeftInv (x : S.leftInv) :
 @[to_additive]
 theorem leftInvEquiv_mul (x : S.leftInv) : (S.leftInvEquiv hS x : M) * x = 1 := by
   simpa only [leftInvEquiv_apply, fromCommLeftInv] using fromLeftInv_mul S x
-
 #align submonoid.left_inv_equiv_mul Submonoid.leftInvEquiv_mul
 #align add_submonoid.left_neg_equiv_add AddSubmonoid.leftNegEquiv_add
 
diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean
index 8e8bad0153459..cf78dafaa8d70 100644
--- a/Mathlib/Topology/Order.lean
+++ b/Mathlib/Topology/Order.lean
@@ -379,7 +379,7 @@ theorem isClosed_induced_iff [t : TopologicalSpace β] {s : Set α} {f : α →
 #align is_closed_induced_iff isClosed_induced_iff
 
 /-- Given `f : α → β` and a topology on `α`, the coinduced topology on `β` is defined
-  such that `s:set β` is open if the preimage of `s` is open. This is the finest topology that
+  such that `s : Set β` is open if the preimage of `s` is open. This is the finest topology that
   makes `f` continuous. -/
 def TopologicalSpace.coinduced {α : Type u} {β : Type v} (f : α → β) (t : TopologicalSpace α) :
     TopologicalSpace β where
@@ -914,10 +914,10 @@ theorem nhds_false : 𝓝 False = ⊤ :=
 #align nhds_false nhds_false
 
 theorem continuous_Prop {p : α → Prop} : Continuous p ↔ IsOpen { x | p x } :=
-  ⟨fun h : Continuous p =>
-    by
+  ⟨fun h : Continuous p => by
     have : IsOpen (p ⁻¹' {True}) := isOpen_singleton_true.preimage h
-    simpa [preimage] using this, fun h : IsOpen { x | p x } =>
+    simpa [preimage] using this,
+   fun h : IsOpen { x | p x } =>
     continuous_generateFrom fun s (hs : s = {True}) => by simp [hs, preimage, h]⟩
 #align continuous_Prop continuous_Prop