chore: tidy various files (#13562)

Author: Ruben-VandeVelde

Mathlib/Algebra/DirectLimit.lean

@@ -703,7 +703,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
   · rintro x (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩)
     · refine
         ⟨j, {⟨i, x⟩, ⟨j, f' i j hij x⟩}, ?_,
-          isSupported_sub (isSupported_of.2 <| Or.inr (by exact rfl))
+          isSupported_sub (isSupported_of.2 <| Or.inr (Set.mem_singleton _))
             (isSupported_of.2 <| Or.inl rfl), fun [_] => ?_⟩
       · rintro k (rfl | ⟨rfl | _⟩)
         · exact hij
@@ -716,7 +716,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
           rw [this]
           · exact sub_self _
         exacts [Or.inl rfl, Or.inr rfl]
-    · refine ⟨i, {⟨i, 1⟩}, ?_, isSupported_sub (isSupported_of.2 (by exact rfl))
+    · refine ⟨i, {⟨i, 1⟩}, ?_, isSupported_sub (isSupported_of.2 (Set.mem_singleton _))
         isSupported_one, fun [_] => ?_⟩
       · rintro k (rfl | h)
         rfl
@@ -728,7 +728,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
         ⟨i, {⟨i, x + y⟩, ⟨i, x⟩, ⟨i, y⟩}, ?_,
           isSupported_sub (isSupported_of.2 <| Or.inl rfl)
             (isSupported_add (isSupported_of.2 <| Or.inr <| Or.inl rfl)
-              (isSupported_of.2 <| Or.inr <| Or.inr (by exact rfl))),
+              (isSupported_of.2 <| Or.inr <| Or.inr (Set.mem_singleton _))),
           fun [_] => ?_⟩
       · rintro k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩) <;> rfl
       · rw [(restriction _).map_sub, (restriction _).map_add, restriction_of, restriction_of,
@@ -743,7 +743,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
         ⟨i, {⟨i, x * y⟩, ⟨i, x⟩, ⟨i, y⟩}, ?_,
           isSupported_sub (isSupported_of.2 <| Or.inl rfl)
             (isSupported_mul (isSupported_of.2 <| Or.inr <| Or.inl rfl)
-              (isSupported_of.2 <| Or.inr <| Or.inr (by exact rfl))), fun [_] => ?_⟩
+              (isSupported_of.2 <| Or.inr <| Or.inr (Set.mem_singleton _))), fun [_] => ?_⟩
       · rintro k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩) <;> rfl
       · rw [(restriction _).map_sub, (restriction _).map_mul, restriction_of, restriction_of,
           restriction_of, dif_pos, dif_pos, dif_pos, RingHom.map_sub,

Mathlib/Algebra/Lie/Submodule.lean

@@ -64,7 +64,7 @@ instance : AddSubgroupClass (LieSubmodule R L M) M where
   zero_mem N := N.zero_mem'
   neg_mem {N} x hx := show -x ∈ N.toSubmodule from neg_mem hx
 
-instance instSmulMemClass : SMulMemClass (LieSubmodule R L M) R M where
+instance instSMulMemClass : SMulMemClass (LieSubmodule R L M) R M where
   smul_mem {s} c _ h := s.smul_mem'  c h
 
 /-- The zero module is a Lie submodule of any Lie module. -/

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -311,7 +311,7 @@ to prove:
 - for all `m₁, m₂`, `P m₁` and `P m₂` implies `P (m₁ + m₂)`;
 - `P 0`.
 
-To invoke this induction principal, use `induction x, hx using Submodule.set_smul_inductionOn` where
+To invoke this induction principle, use `induction x, hx using Submodule.set_smul_inductionOn` where
 `x : M` and `hx : x ∈ s • N`
 
 When we consider subset of `R` acting on `M`
@@ -408,14 +408,14 @@ theorem span_set_smul [SMulCommClass S R M] (s : Set S) (t : Set M) :
 
 variable {s N} in
 /--
-Induction principal for set acting on submodules. To prove `P` holds for all `s • N`, it is enough
+Induction principle for set acting on submodules. To prove `P` holds for all `s • N`, it is enough
 to prove:
 - for all `r ∈ s` and `n ∈ N`, `P (r • n)`;
 - for all `r` and `m ∈ s • N`, `P (r • n)`;
 - for all `m₁, m₂`, `P m₁` and `P m₂` implies `P (m₁ + m₂)`;
 - `P 0`.
 
-To invoke this induction principal, use `induction x, hx using Submodule.set_smul_inductionOn` where
+To invoke this induction principle, use `induction x, hx using Submodule.set_smul_inductionOn` where
 `x : M` and `hx : x ∈ s • N`
 -/
 @[elab_as_elim]

Mathlib/Algebra/MonoidAlgebra/Ideal.lean

@@ -35,10 +35,7 @@ theorem MonoidAlgebra.mem_ideal_span_of_image [Monoid G] [Semiring k] {s : Set G
         obtain ⟨xm, -, hm⟩ := hm
         replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
         obtain ⟨ym, hym, hm⟩ := hm
-        replace hm := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
-        obtain rfl := hm
-        -- Porting note: changed `Exists.imp` to `And.imp_right` due to change in `∃ x ∈ s`
-        -- elaboration
+        obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
         refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
         rintro ⟨d, rfl⟩
         exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -20,7 +20,7 @@ We use eight typeclasses to encode the various properties we care about for thos
 These typeclasses are meant to be mostly internal to this file, to set up each lemma in the
 appropriate generality.
 
-Less granular typeclasses like `OrderedAddCommMonoid`, `LinearOrderedField`` should be enough for
+Less granular typeclasses like `OrderedAddCommMonoid`, `LinearOrderedField` should be enough for
 most purposes, and the system is set up so that they imply the correct granular typeclasses here.
 If those are enough for you, you may stop reading here! Else, beware that what follows is a bit
 technical.

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

@@ -168,20 +168,20 @@ instance lift_comp_eqToHom {R S S': 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶
 @[simp]
 lemma comp_eqToHom_lift_iff {R S : 𝒮} {a' a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : a' = a) :
     p.IsHomLift f (eqToHom h ≫ φ) ↔ p.IsHomLift f φ where
-  mp := fun hφ' => by subst h; simpa using hφ'
-  mpr := fun hφ => inferInstance
+  mp hφ' := by subst h; simpa using hφ'
+  mpr hφ := inferInstance
 
 @[simp]
 lemma eqToHom_comp_lift_iff {R S : 𝒮} {a b b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b') :
     p.IsHomLift f (φ ≫ eqToHom h) ↔ p.IsHomLift f φ where
-  mp := fun hφ' => by subst h; simpa using hφ'
-  mpr := fun hφ => inferInstance
+  mp hφ' := by subst h; simpa using hφ'
+  mpr hφ := inferInstance
 
 @[simp]
 lemma lift_eqToHom_comp_iff {R' R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : R' = R) :
     p.IsHomLift (eqToHom h ≫ f) φ ↔ p.IsHomLift f φ where
-  mp := fun hφ' => by subst h; simpa using hφ'
-  mpr := fun hφ => inferInstance
+  mp hφ' := by subst h; simpa using hφ'
+  mpr hφ := inferInstance
 
 @[simp]
 lemma lift_comp_eqToHom_iff {R S S' : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S') :

Mathlib/CategoryTheory/IsConnected.lean

@@ -120,8 +120,9 @@ theorem any_functor_const_on_obj [IsPreconnected J] {α : Type u₂} (F : J ⥤
 /-- If any functor to a discrete category is constant on objects, J is connected.
 The converse of `any_functor_const_on_obj`.
 -/
-theorem IsPreconnected.of_any_functor_const_on_obj (h : ∀ {α : Type u₁} (F : J ⥤ Discrete α),
-    ∀ j j' : J, F.obj j = F.obj j') : IsPreconnected J where
+theorem IsPreconnected.of_any_functor_const_on_obj
+    (h : ∀ {α : Type u₁} (F : J ⥤ Discrete α), ∀ j j' : J, F.obj j = F.obj j') :
+    IsPreconnected J where
   iso_constant := fun F j' => ⟨NatIso.ofComponents fun j => eqToIso (h F j j')⟩
 
 /-- If any functor to a discrete category is constant on objects, J is connected.
@@ -143,11 +144,7 @@ theorem constant_of_preserves_morphisms [IsPreconnected J] {α : Type u₂} (F :
   simpa using
     any_functor_const_on_obj
       { obj := Discrete.mk ∘ F
-        map := @fun _ _ f =>
-          eqToHom
-            (by
-              ext
-              exact h _ _ f) }
+        map := fun f => eqToHom (by ext; exact h _ _ f) }
       j j'
 #align category_theory.constant_of_preserves_morphisms CategoryTheory.constant_of_preserves_morphisms
 
@@ -161,7 +158,7 @@ theorem IsPreconnected.of_constant_of_preserves_morphisms
     (h : ∀ {α : Type u₁} (F : J → α),
       (∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ j j' : J, F j = F j') :
     IsPreconnected J :=
-  IsPreconnected.of_any_functor_const_on_obj @fun _ F =>
+  IsPreconnected.of_any_functor_const_on_obj fun F =>
     h F.obj fun f => by ext; exact Discrete.eq_of_hom (F.map f)
 
 /-- `J` is connected if: given any function `F : J → α` which is constant for any
@@ -215,8 +212,7 @@ instance [hc : IsConnected J] : IsConnected (ULiftHom.{v₂} (ULift.{u₂} J)) :
     have hj₀' : Classical.choice hc.is_nonempty ∈ p' := by
       simp only [p', (eq_self p')]
       exact hj₀
-    apply induct_on_objects p' hj₀' @fun _ _ f =>
-      h ((ULiftHomULiftCategory.equiv J).functor.map f)
+    apply induct_on_objects p' hj₀' fun f => h ((ULiftHomULiftCategory.equiv J).functor.map f)
 
 /-- Another induction principle for `IsPreconnected J`:
 given a type family `Z : J → Sort*` and
@@ -227,14 +223,8 @@ theorem isPreconnected_induction [IsPreconnected J] (Z : J → Sort*)
     (h₁ : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), Z j₁ → Z j₂) (h₂ : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), Z j₂ → Z j₁)
     {j₀ : J} (x : Z j₀) (j : J) : Nonempty (Z j) :=
   (induct_on_objects { j | Nonempty (Z j) } ⟨x⟩
-      (fun f =>
-        ⟨by
-          rintro ⟨y⟩
-          exact ⟨h₁ f y⟩, by
-          rintro ⟨y⟩
-          exact ⟨h₂ f y⟩⟩)
-      j :
-    _)
+      (fun f => ⟨by rintro ⟨y⟩; exact ⟨h₁ f y⟩, by rintro ⟨y⟩; exact ⟨h₂ f y⟩⟩)
+      j : _)
 #align category_theory.is_preconnected_induction CategoryTheory.isPreconnected_induction
 
 /-- If `J` and `K` are equivalent, then if `J` is preconnected then `K` is as well. -/
@@ -385,7 +375,7 @@ theorem equiv_relation [IsPreconnected J] (r : J → J → Prop) (hr : _root_.Eq
 /-- In a connected category, any two objects are related by `Zigzag`. -/
 theorem isPreconnected_zigzag [IsPreconnected J] (j₁ j₂ : J) : Zigzag j₁ j₂ :=
   equiv_relation _ zigzag_equivalence
-    (@fun _ _ f => Relation.ReflTransGen.single (Or.inl (Nonempty.intro f))) _ _
+    (fun f => Relation.ReflTransGen.single (Or.inl (Nonempty.intro f))) _ _
 #align category_theory.is_connected_zigzag CategoryTheory.isPreconnected_zigzag
 
 @[deprecated (since := "2024-02-19")] alias isConnected_zigzag := isPreconnected_zigzag
@@ -466,9 +456,11 @@ instance [IsConnected J] : (Functor.const J : C ⥤ J ⥤ C).Full where
 
 theorem nonempty_hom_of_preconnected_groupoid {G} [Groupoid G] [IsPreconnected G] :
     ∀ x y : G, Nonempty (x ⟶ y) := by
-  refine equiv_relation _ ?_ @fun j₁ j₂ => Nonempty.intro
+  refine equiv_relation _ ?_ fun {j₁ j₂} => Nonempty.intro
   exact
-    ⟨fun j => ⟨𝟙 _⟩, @fun j₁ j₂ => Nonempty.map fun f => inv f, @fun _ _ _ => Nonempty.map2 (· ≫ ·)⟩
+    ⟨fun j => ⟨𝟙 _⟩,
+     fun {j₁ j₂} => Nonempty.map fun f => inv f,
+     fun {_ _ _} => Nonempty.map2 (· ≫ ·)⟩
 #align category_theory.nonempty_hom_of_connected_groupoid CategoryTheory.nonempty_hom_of_preconnected_groupoid
 
 attribute [instance] nonempty_hom_of_preconnected_groupoid

Mathlib/CategoryTheory/Localization/Triangulated.lean

@@ -190,7 +190,8 @@ def pretriangulated : Pretriangulated D where
 
 instance isTriangulated_functor :
     letI : Pretriangulated D := pretriangulated L W; L.IsTriangulated :=
-    letI : Pretriangulated D := pretriangulated L W; ⟨fun T hT => ⟨T, Iso.refl _, hT⟩⟩
+  letI : Pretriangulated D := pretriangulated L W
+  ⟨fun T hT => ⟨T, Iso.refl _, hT⟩⟩
 
 lemma isTriangulated [Pretriangulated D] [L.IsTriangulated] [IsTriangulated C] :
     IsTriangulated D := by

Mathlib/Data/Finsupp/Defs.lean

@@ -458,7 +458,9 @@ lemma apply_single [AddCommMonoid N] [AddCommMonoid P]
     e ((single a n) b) = single a (e n) b := by
   classical
   simp only [single_apply]
-  split_ifs; rfl; exact map_zero e
+  split_ifs
+  · rfl
+  · exact map_zero e
 
 theorem support_eq_singleton {f : α →₀ M} {a : α} :
     f.support = {a} ↔ f a ≠ 0 ∧ f = single a (f a) :=

Mathlib/Data/Prod/Lex.lean

@@ -104,7 +104,7 @@ instance preorder (α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×
 
 theorem monotone_fst [Preorder α] [LE β] (t c : α ×ₗ β) (h : t ≤ c) :
     (ofLex t).1 ≤ (ofLex c).1 := by
-  cases ((Prod.Lex.le_iff t c).mp h) with
+  cases (Prod.Lex.le_iff t c).mp h with
   | inl h' => exact h'.le
   | inr h' => exact h'.1.le