chore: tidy various files (#2321)

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,18 +530,18 @@ 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."
 
 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,23 +562,23 @@ 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
 
 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
-

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⟩

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) :