chore: tidy various files (#2446)

Mathlib/Algebra/Algebra/Basic.lean

@@ -93,7 +93,7 @@ all be relaxed independently; for instance, this allows us to:
   which when `R' = Rˣ` lets us talk about the "algebra-like" action of `Rˣ` on an
   `R`-algebra `A`.
 
-While `alg_hom R A B` cannot be used in the second approach, `non_unital_alg_hom R A B` still can.
+While `AlgHom R A B` cannot be used in the second approach, `NonUnitalAlgHom R A B` still can.
 
 You should always use the first approach when working with associative unital algebras, and mimic
 the second approach only when you need to weaken a condition on either `R` or `A`.
@@ -249,9 +249,9 @@ variable (R A : Type _) [Field R] [DivisionRing A] [Algebra R A]
 
 -- porting note: todo: drop implicit args
 @[norm_cast]
-theorem coe_rat_cast (q : ℚ) : ↑(q : R) = (q : A) :=
+theorem coe_ratCast (q : ℚ) : ↑(q : R) = (q : A) :=
   @map_ratCast (R →+* A) R A _ _ _ (algebraMap R A) q
-#align algebra_map.coe_rat_cast algebraMap.coe_rat_cast
+#align algebra_map.coe_rat_cast algebraMap.coe_ratCast
 
 end FieldDivisionRing
 
@@ -384,7 +384,7 @@ instance _root_.IsScalarTower.right : IsScalarTower R A A :=
   ⟨fun x y z => by rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]⟩
 #align is_scalar_tower.right IsScalarTower.right
 
--- TODO: set up `is_scalar_tower.smul_comm_class` earlier so that we can actually prove this using
+-- TODO: set up `IsScalarTower.smulCommClass` earlier so that we can actually prove this using
 -- `mul_smul_comm s x y`.
 
 /-- This is just a special case of the global `mul_smul_comm` lemma that requires less typeclass
@@ -485,8 +485,7 @@ section ULift
 
 instance _root_.ULift.algebra : Algebra R (ULift A) :=
   { ULift.module',
-    (ULift.ringEquiv : ULift A ≃+* A).symm.toRingHom.comp
-      (algebraMap R A) with
+    (ULift.ringEquiv : ULift A ≃+* A).symm.toRingHom.comp (algebraMap R A) with
     toFun := fun r => ULift.up (algebraMap R A r)
     commutes' := fun r x => ULift.down_injective <| Algebra.commutes r x.down
     smul_def' := fun r x => ULift.down_injective <| Algebra.smul_def' r x.down }
@@ -504,7 +503,7 @@ theorem _root_.ULift.down_algebraMap (r : R) : (algebraMap R (ULift A) r).down =
 
 end ULift
 
-/-- Algebra over a subsemiring. This builds upon `subsemiring.module`. -/
+/-- Algebra over a subsemiring. This builds upon `Subsemiring.module`. -/
 instance ofSubsemiring (S : Subsemiring R) : Algebra S A where
   toRingHom := (algebraMap R A).comp S.subtype
   smul := (· • ·)
@@ -525,7 +524,7 @@ theorem algebraMap_ofSubsemiring_apply (S : Subsemiring R) (x : S) : algebraMap
   rfl
 #align algebra.algebra_map_of_subsemiring_apply Algebra.algebraMap_ofSubsemiring_apply
 
-/-- Algebra over a subring. This builds upon `subring.module`. -/
+/-- Algebra over a subring. This builds upon `Subring.module`. -/
 instance ofSubring {R A : Type _} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) :
     Algebra S A where -- porting note: don't use `toSubsemiring` because of a timeout
   toRingHom := (algebraMap R A).comp S.subtype
@@ -604,11 +603,11 @@ variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
 
 instance : Algebra R Aᵐᵒᵖ where
   toRingHom := (algebraMap R A).toOpposite fun x y => Algebra.commutes _ _
-  smul_def' := fun c x => unop_injective <| by
-    dsimp
-    simp only [op_mul, Algebra.smul_def, Algebra.commutes, op_unop]
-  commutes' := fun r => MulOpposite.rec' fun x => by
-    dsimp; simp only [← op_mul, Algebra.commutes]
+  smul_def' c x := unop_injective <| by
+    simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul,
+      Algebra.smul_def, Algebra.commutes, op_unop]
+  commutes' r := MulOpposite.rec' fun x => by
+    simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]
 
 @[simp]
 theorem algebraMap_apply (c : R) : algebraMap R Aᵐᵒᵖ c = op (algebraMap R A c) :=
@@ -720,7 +719,7 @@ variable {R : Type _} [Semiring R]
 
 -- Lower the priority so that `Algebra.id` is picked most of the time when working with
 -- `ℕ`-algebras. This is only an issue since `Algebra.id` and `algebraNat` are not yet defeq.
--- TODO: fix this by adding an `of_nat` field to semirings.
+-- TODO: fix this by adding an `ofNat` field to semirings.
 /-- Semiring ⥤ ℕ-Alg -/
 instance (priority := 99) algebraNat : Algebra ℕ R where
   commutes' := Nat.cast_commute
@@ -776,7 +775,7 @@ variable (R : Type _) [Ring R]
 
 -- Lower the priority so that `Algebra.id` is picked most of the time when working with
 -- `ℤ`-algebras. This is only an issue since `Algebra.id ℤ` and `algebraInt ℤ` are not yet defeq.
--- TODO: fix this by adding an `of_int` field to rings.
+-- TODO: fix this by adding an `ofInt` field to rings.
 /-- Ring ⥤ ℤ-Alg -/
 instance (priority := 99) algebraInt : Algebra ℤ R where
   commutes' := Int.cast_commute
@@ -807,7 +806,7 @@ open Algebra
 /-- If `algebraMap R A` is injective and `A` has no zero divisors,
 `R`-multiples in `A` are zero only if one of the factors is zero.
 
-Cannot be an instance because there is no `injective (algebraMap R A)` typeclass.
+Cannot be an instance because there is no `Injective (algebraMap R A)` typeclass.
 -/
 theorem of_algebraMap_injective [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A]
     (h : Function.Injective (algebraMap R A)) : NoZeroSMulDivisors R A :=
@@ -881,10 +880,10 @@ theorem algebraMap_smul (r : R) (m : M) : (algebraMap R A) r • m = r • m :=
   (algebra_compatible_smul A r m).symm
 #align algebra_map_smul algebraMap_smul
 
-theorem int_cast_smul {k V : Type _} [CommRing k] [AddCommGroup V] [Module k V] (r : ℤ) (x : V) :
+theorem intCast_smul {k V : Type _} [CommRing k] [AddCommGroup V] [Module k V] (r : ℤ) (x : V) :
     (r : k) • x = r • x :=
   algebraMap_smul k r x
-#align int_cast_smul int_cast_smul
+#align int_cast_smul intCast_smul
 
 theorem NoZeroSMulDivisors.trans (R A M : Type _) [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
     [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors R A]
@@ -910,9 +909,9 @@ instance (priority := 100) IsScalarTower.to_sMulCommClass : SMulCommClass R A M
 #align is_scalar_tower.to_smul_comm_class IsScalarTower.to_sMulCommClass
 
 -- see Note [lower instance priority]
-instance (priority := 100) IsScalarTower.to_smul_comm_class' : SMulCommClass A R M :=
+instance (priority := 100) IsScalarTower.to_sMulCommClass' : SMulCommClass A R M :=
   SMulCommClass.symm _ _ _
-#align is_scalar_tower.to_smul_comm_class' IsScalarTower.to_smul_comm_class'
+#align is_scalar_tower.to_smul_comm_class' IsScalarTower.to_sMulCommClass'
 
 theorem smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
   smul_comm _ _ _
@@ -940,8 +939,8 @@ end LinearMap
 end IsScalarTower
 
 /-! TODO: The following lemmas no longer involve `Algebra` at all, and could be moved closer
-to `Algebra/Module/submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
-are all defined in `linear_algebra/basic.lean`. -/
+to `Algebra/Module/Submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
+are all defined in `LinearAlgebra/Basic.lean`. -/
 
 section Module
 

Mathlib/CategoryTheory/Arrow.lean

@@ -37,11 +37,11 @@ variable (T)
 /-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative
      squares in `T`. -/
 def Arrow :=
-  Comma.{v, v, v} (𝟭 T) (𝟭 T) 
+  Comma.{v, v, v} (𝟭 T) (𝟭 T)
 #align category_theory.arrow CategoryTheory.Arrow
 
 /- Porting note: could not derive `Category` above so this instance works in its place-/
-instance : Category (Arrow T) := commaCategory 
+instance : Category (Arrow T) := commaCategory
 
 -- Satisfying the inhabited linter
 instance Arrow.inhabited [Inhabited T] : Inhabited (Arrow T)
@@ -87,8 +87,8 @@ theorem mk_inj (A B : T) {f g : A ⟶ B} : Arrow.mk f = Arrow.mk g ↔ f = g :=
 #align category_theory.arrow.mk_inj CategoryTheory.Arrow.mk_inj
 
 /- Porting note : was marked as dangerous instance so changed from `Coe` to `CoeOut` -/
-instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where 
-  coe := mk 
+instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where
+  coe := mk
 
 /-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
     category. -/
@@ -109,7 +109,7 @@ def homMk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y
   w := w
 #align category_theory.arrow.hom_mk' CategoryTheory.Arrow.homMk'
 
-/- Porting note : was warned simp could prove reassoc'd version. Found simp could not. 
+/- Porting note : was warned simp could prove reassoc'd version. Found simp could not.
 Added nolint. -/
 @[reassoc (attr := simp, nolint simpNF)]
 theorem w {f g : Arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right :=
@@ -124,15 +124,15 @@ theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) :
 #align category_theory.arrow.w_mk_right CategoryTheory.Arrow.w_mk_right
 
 theorem isIso_of_iso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
-    [IsIso ff.right] : IsIso ff where 
-  out := by 
-    let inverse : g ⟶  f := ⟨inv ff.left, inv ff.right, (by simp)⟩ 
+    [IsIso ff.right] : IsIso ff where
+  out := by
+    let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
     apply Exists.intro inverse
     constructor
     · apply CommaMorphism.ext
       · rw [Comma.comp_left, IsIso.hom_inv_id, ←Comma.id_left]
       · rw [Comma.comp_right, IsIso.hom_inv_id, ←Comma.id_right]
-    · apply CommaMorphism.ext 
+    · apply CommaMorphism.ext
       · rw [Comma.comp_left, IsIso.inv_hom_id, ←Comma.id_left]
       · rw [Comma.comp_right, IsIso.inv_hom_id, ←Comma.id_right]
 #align category_theory.arrow.is_iso_of_iso_left_of_is_iso_right CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right
@@ -177,20 +177,20 @@ section
 
 variable {f g : Arrow T} (sq : f ⟶ g)
 
-instance isIso_left [IsIso sq] : IsIso sq.left where 
-  out := by 
-    apply Exists.intro (inv sq).left 
+instance isIso_left [IsIso sq] : IsIso sq.left where
+  out := by
+    apply Exists.intro (inv sq).left
     simp only [← Comma.comp_left, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_left,
       eq_self_iff_true, and_self_iff]
-    simp 
+    simp
 #align category_theory.arrow.is_iso_left CategoryTheory.Arrow.isIso_left
 
-instance isIso_right [IsIso sq] : IsIso sq.right where 
-  out := by 
+instance isIso_right [IsIso sq] : IsIso sq.right where
+  out := by
     apply Exists.intro (inv sq).right
     simp only [← Comma.comp_right, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_right,
       eq_self_iff_true, and_self_iff]
-    simp 
+    simp
 #align category_theory.arrow.is_iso_right CategoryTheory.Arrow.isIso_right
 
 @[simp]
@@ -213,24 +213,23 @@ theorem inv_left_hom_right [IsIso sq] : inv sq.left ≫ f.hom ≫ sq.right = g.h
   simp only [w, IsIso.inv_comp_eq]
 #align category_theory.arrow.inv_left_hom_right CategoryTheory.Arrow.inv_left_hom_right
 
-instance mono_left [Mono sq] : Mono sq.left where 
-  right_cancellation {Z} φ ψ h :=
-    by
+instance mono_left [Mono sq] : Mono sq.left where
+  right_cancellation {Z} φ ψ h := by
     let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
       { left := φ
         right := φ ≫ f.hom }
-    have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp   
+    have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp
     show (aux φ).left = (aux ψ).left
     congr 1
     rw [← cancel_mono sq]
     apply CommaMorphism.ext
     · exact h
-    · rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc] 
+    · rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc]
       rw [←Arrow.w]
       simp only [← Category.assoc, h]
 #align category_theory.arrow.mono_left CategoryTheory.Arrow.mono_left
 
-instance epi_right [Epi sq] : Epi sq.right where 
+instance epi_right [Epi sq] : Epi sq.right where
   left_cancellation {Z} φ ψ h := by
     let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ =>
       { right := φ
@@ -303,8 +302,7 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
 /-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories. -/
 @[simps]
-def mapArrow (F : C ⥤ D) : Arrow C ⥤ Arrow D
-    where
+def mapArrow (F : C ⥤ D) : Arrow C ⥤ Arrow D where
   obj a :=
     { left := F.obj a.left
       right := F.obj a.right
@@ -317,8 +315,8 @@ def mapArrow (F : C ⥤ D) : Arrow C ⥤ Arrow D
         simp only [id_map] at w
         dsimp
         simp only [← F.map_comp, w] }
-  map_id := by aesop_cat 
-  map_comp := fun f g => by 
+  map_id := by aesop_cat
+  map_comp := fun f g => by
     apply CommaMorphism.ext
     · dsimp; rw [Comma.comp_left,F.map_comp]; rw [Comma.comp_left]
     · dsimp; rw [Comma.comp_right,F.map_comp]; rw [Comma.comp_right]
@@ -332,6 +330,5 @@ def Arrow.isoOfNatIso {C D : Type _} [Category C] [Category D] {F G : C ⥤ D} (
     (f : Arrow C) : F.mapArrow.obj f ≅ G.mapArrow.obj f :=
   Arrow.isoMk (e.app f.left) (e.app f.right) (by simp)
 #align category_theory.arrow.iso_of_nat_iso CategoryTheory.Arrow.isoOfNatIso
- 
+
 end CategoryTheory
-#lint

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -41,16 +41,15 @@ open CategoryTheory
 The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.
 
 Because we don't allow morphisms to live in `Prop`,
-we have to define `X ⟶ Y` as `ulift (plift (X ≤ Y))`.
+we have to define `X ⟶ Y` as `ULift (PLift (X ≤ Y))`.
 See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`.
 
 See <https://stacks.math.columbia.edu/tag/00D3>.
 -/
-instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α
-    where
+instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α where
   Hom U V := ULift (PLift (U ≤ V))
   id X := ⟨⟨le_refl X⟩⟩
-  comp := @fun X Y Z f g => ⟨⟨le_trans _ _ _ f.down.down g.down.down⟩⟩
+  comp f g := ⟨⟨le_trans _ _ _ f.down.down g.down.down⟩⟩
 #align preorder.small_category Preorder.smallCategory
 
 end Preorder
@@ -96,11 +95,10 @@ theorem leOfHom_homOfLE {x y : X} (h : x ≤ y) : h.hom.le = h :=
   rfl
 #align category_theory.le_of_hom_hom_of_le CategoryTheory.leOfHom_homOfLE
 
--- porting note: why does this lemma exist? With proof irrelevance, we don't need to simplify proofs
+-- 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
 -- @[simp]
-theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h := by
-  cases' h with h
-  cases h
+theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h :=
   rfl
 #align category_theory.hom_of_le_le_of_hom CategoryTheory.homOfLE_leOfHom
 

Mathlib/CategoryTheory/Core.lean

@@ -42,10 +42,10 @@ def Core (C : Type u₁) := C
 variable {C : Type u₁} [Category.{v₁} C]
 
 instance coreCategory : Groupoid.{v₁} (Core C) where
-  Hom := fun X Y : C => X ≅ Y
-  id := fun X => @Iso.refl C _ X
-  comp := @fun {X} {Y} {Z} f g => Iso.trans f g
-  inv := @fun X Y f => Iso.symm f
+  Hom (X Y : C) := X ≅ Y
+  id (X : C) := Iso.refl X
+  comp f g := Iso.trans f g
+  inv {X Y} f := Iso.symm f
 #align category_theory.core_category CategoryTheory.coreCategory
 
 namespace Core
@@ -66,7 +66,7 @@ variable (C)
 /-- The core of a category is naturally included in the category. -/
 def inclusion : Core C ⥤ C where
   obj := id
-  map := @fun X Y f => f.hom
+  map f := f.hom
 #align category_theory.core.inclusion CategoryTheory.Core.inclusion
 
 -- porting note: This worked wihtout proof before.
@@ -80,10 +80,9 @@ variable {C} {G : Type u₂} [Groupoid.{v₂} G]
 -- Note that this function is not functorial
 -- (consider the two functors from [0] to [1], and the natural transformation between them).
 /-- A functor from a groupoid to a category C factors through the core of C. -/
-noncomputable def functorToCore (F : G ⥤ C) : G ⥤ Core C
-    where
+noncomputable def functorToCore (F : G ⥤ C) : G ⥤ Core C where
   obj X := F.obj X
-  map := @fun X Y f => ⟨F.map f, F.map (inv f), _, _⟩
+  map f := ⟨F.map f, F.map (inv f), _, _⟩
 #align category_theory.core.functor_to_core CategoryTheory.Core.functorToCore
 
 /-- We can functorially associate to any functor from a groupoid to the core of a category `C`,
@@ -101,10 +100,10 @@ to a categorical functor `Core (Type u₁) ⥤ Core (Type u₂)`.
 def ofEquivFunctor (m : Type u₁ → Type u₂) [EquivFunctor m] : Core (Type u₁) ⥤ Core (Type u₂)
     where
   obj := m
-  map := @fun α β f => (EquivFunctor.mapEquiv m f.toEquiv).toIso
+  map f := (EquivFunctor.mapEquiv m f.toEquiv).toIso
   map_id α := by apply Iso.ext; funext x; exact congr_fun (EquivFunctor.map_refl' _) x
-  map_comp := @fun α β γ f g => by
-    apply Iso.ext; funext x; dsimp;
+  map_comp f g := by
+    apply Iso.ext; funext x; dsimp
     erw [Iso.toEquiv_comp, EquivFunctor.map_trans']
     rw [Function.comp]
 #align category_theory.of_equiv_functor CategoryTheory.ofEquivFunctor