chore: tidy various files (#14485)

Author: Ruben-VandeVelde

Mathlib/Algebra/Group/Action/Opposite.lean

@@ -154,7 +154,7 @@ open MulOpposite
 See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`. -/
 @[to_additive "Like `Add.toVAdd`, but adds on the right.
 
-  See also `AddMonoid.to_OppositeAddAction`."]
+  See also `AddMonoid.toOppositeAddAction`."]
 instance Mul.toHasOppositeSMul [Mul α] : SMul αᵐᵒᵖ α where smul c x := x * c.unop
 #align has_mul.to_has_opposite_smul Mul.toHasOppositeSMul
 #align has_add.to_has_opposite_vadd Add.toHasOppositeVAdd

Mathlib/Analysis/Convex/Radon.lean

@@ -89,13 +89,11 @@ theorem helly_theorem' {F : ι → Set E} {s : Finset ι}
   /- Construct a family of vectors indexed by `ι` such that the vector corresponding to `i : ι`
   is an arbitrary element of the intersection of all `F j` except `F i`. -/
   let a (i : s) : E := Set.Nonempty.some (s := ⋂ j ∈ (s.erase i), F j) <| by
-    let s' :=  s.erase i
-    apply hk (s := s')
-    · exact fun i hi ↦h_convex i (mem_of_mem_erase hi)
+    apply hk (s := s.erase i)
+    · exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
     · intro J hJ_ss hJ_card
-      apply h_inter J <| subset_trans hJ_ss (erase_subset i.val s)
-      assumption
-    · simp only [coe_mem, card_erase_of_mem, s']; omega
+      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
+    · simp only [coe_mem, card_erase_of_mem]; omega
   /- This family of vectors is not affine independent because the number of them exceeds the
   dimension of the space. -/
   have h_ind : ¬AffineIndependent 𝕜 a := by
@@ -145,7 +143,7 @@ theorem helly_theorem {F : ι → Set E} {s : Finset ι}
   apply helly_theorem' h_convex
   intro I hI_ss hI_card
   obtain ⟨J, hI_ss_J, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card
-  apply Set.Nonempty.mono <| biInter_mono hI_ss_J (by intro _ _; rfl)
+  apply Set.Nonempty.mono <| biInter_mono hI_ss_J (fun _ _ ↦ Set.Subset.rfl)
   exact h_inter J hJ_ss hJ_card
 
 /-- **Helly's theorem** for finite sets of convex sets.
@@ -190,7 +188,7 @@ theorem helly_theorem_compact' [TopologicalSpace E] [T2Space E] {F : ι → Set
     (⋂ i, F i).Nonempty := by
   /- If `ι` is empty the statement is trivial. -/
   cases' isEmpty_or_nonempty ι with _ h_nonempty
-  simp only [iInter_of_empty, Set.univ_nonempty]
+  · simp only [iInter_of_empty, Set.univ_nonempty]
   /- By the finite version of theorem, every finite subfamily has an intersection. -/
   have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty := by
     apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])

Mathlib/CategoryTheory/Monad/Coequalizer.lean

@@ -19,7 +19,8 @@ In `C`, this cofork diagram is a split coequalizer (in particular, it is still a
 This split coequalizer is known as the Beck coequalizer (as it features heavily in Beck's
 monadicity theorem).
 
-This file has been adapted to `CategoryTheory.Monad.Equalizer`. Please try to keep them in sync.
+This file has been adapted to `Mathlib.CategoryTheory.Monad.Equalizer`.
+Please try to keep them in sync.
 
 -/
 

Mathlib/CategoryTheory/Monad/Equalizer.lean

@@ -17,7 +17,8 @@ In `C`, this fork diagram is a split equalizer (in particular, it is still an eq
 This split equalizer is known as the Beck equalizer (as it features heavily in Beck's
 comonadicity theorem).
 
-This file is adapted from `CategoryTheory.Monad.Coequalizer`. Please try to keep them in sync.
+This file is adapted from `Mathlib.CategoryTheory.Monad.Coequalizer`.
+Please try to keep them in sync.
 
 -/
 

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -23,7 +23,6 @@ one edge, and the edges of the subgraph represent the paired vertices.
 
 * `SimpleGraph.Subgraph.IsMatching`: `M.IsMatching` means that `M` is a matching of its
   underlying graph.
-  denoted `M.is_matching`.
 
 * `SimpleGraph.Subgraph.IsPerfectMatching` defines when a subgraph `M` of a simple graph is a
   perfect matching, denoted `M.IsPerfectMatching`.
@@ -36,7 +35,7 @@ one edge, and the edges of the subgraph represent the paired vertices.
 
 * Tutte's Theorem
 
-* Hall's Marriage Theorem (see Combinatorics.Hall.Basic)
+* Hall's Marriage Theorem (see `Mathlib.Combinatorics.Hall.Basic`)
 -/
 
 open Function
@@ -156,28 +155,28 @@ lemma even_card_of_isPerfectMatching (c : ConnectedComponent G) (hM : M.IsPerfec
 lemma odd_matches_node_outside {u : Set V} {c : ConnectedComponent (Subgraph.deleteVerts ⊤ u).coe}
     (hM : M.IsPerfectMatching) (codd : Odd (Nat.card c.supp)) :
     ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.supp := by
-    by_contra! h
-    have hMmatch : (M.induce c.supp).IsMatching := by
-      intro v hv
-      obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
-      obtain ⟨⟨v', hv'⟩, ⟨hv , rfl⟩⟩ := hv
-      use w
-      have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
-      refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
-      apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
-      simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and,
-        Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
-        and_true] at hv' ⊢
-      trivial
-
-    apply Nat.odd_iff_not_even.mp codd
-    haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c)).verts := Fintype.ofFinite _
-    have hMeven := Subgraph.IsMatching.even_card hMmatch
-    haveI : Fintype (c.supp) := Fintype.ofFinite _
-    simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_image,
-      Nat.card_eq_fintype_card, Set.toFinset_image,
-      Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card] at hMeven ⊢
-    exact hMeven
+  by_contra! h
+  have hMmatch : (M.induce c.supp).IsMatching := by
+    intro v hv
+    obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
+    obtain ⟨⟨v', hv'⟩, ⟨hv , rfl⟩⟩ := hv
+    use w
+    have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
+    refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
+    apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
+    simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and,
+      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
+      and_true] at hv' ⊢
+    trivial
+
+  apply Nat.odd_iff_not_even.mp codd
+  haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c)).verts := Fintype.ofFinite _
+  have hMeven := Subgraph.IsMatching.even_card hMmatch
+  haveI : Fintype (c.supp) := Fintype.ofFinite _
+  simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_image,
+    Nat.card_eq_fintype_card, Set.toFinset_image,
+    Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card] at hMeven ⊢
+  exact hMeven
 
 end Finite
 end ConnectedComponent

Mathlib/Data/LazyList/Basic.lean

@@ -171,10 +171,10 @@ instance : LawfulMonad LazyList := LawfulMonad.mk'
   (bind_pure_comp := by
     intro _ _ f xs
     simp only [bind, Functor.map, pure, singleton]
-    induction xs using LazyList.traverse.induct (m := @Id) (f := f)
-    case case1 =>
+    induction xs using LazyList.traverse.induct (m := @Id) (f := f) with
+    | case1 =>
       simp only [Thunk.pure, LazyList.bind, LazyList.traverse, Id.pure_eq]
-    case case2 ih =>
+    | case2 _ _ ih =>
       simp only [LazyList.bind, LazyList.traverse, Seq.seq, Id.map_eq, append, Thunk.pure]
       rw [← ih]
       simp [Thunk.pure, Thunk.get, append])

Mathlib/Data/Matroid/Basic.lean

@@ -616,8 +616,8 @@ theorem Indep.exists_insert_of_not_base (hI : M.Indep I) (hI' : ¬M.Base I) (hB
     ∃ e ∈ B \ I, M.Indep (insert e I) := by
   obtain ⟨B', hB', hIB'⟩ := hI.exists_base_superset
   obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))
-  obtain (hxB | hxB) := em (x ∈ B)
-  · exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB') ⟩
+  by_cases hxB : x ∈ B
+  · exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩
   obtain ⟨e,he, hBase⟩ := hB'.exchange hB ⟨hxB',hxB⟩
   exact ⟨e, ⟨he.1, not_mem_subset hIB' he.2⟩,
     indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_diff_singleton hIB' hx)⟩⟩

Mathlib/Data/Matroid/IndepAxioms.lean

@@ -110,7 +110,7 @@ namespace IndepMatroid
   Base := (· ∈ maximals (· ⊆ ·) {I | M.Indep I})
   Indep := M.Indep
   indep_iff' := by
-    refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B,⟨h,_⟩,hIB'⟩ ↦ M.indep_subset h hIB'⟩
+    refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩
     obtain ⟨B, hB⟩ := M.indep_maximal M.E Subset.rfl I h (M.subset_ground I h)
     simp only [mem_maximals_iff, mem_setOf_eq, and_imp] at hB ⊢
     exact ⟨B, ⟨hB.1.1,fun J hJ hBJ ↦ hB.2 hJ (hB.1.2.1.trans hBJ) (M.subset_ground J hJ) hBJ⟩,

Mathlib/Data/Nat/Prime/Defs.lean

@@ -325,12 +325,15 @@ theorem minFac_prime {n : ℕ} (n1 : n ≠ 1) : Prime (minFac n) :=
 #align nat.min_fac_prime Nat.minFac_prime
 
 theorem minFac_le_of_dvd {n : ℕ} : ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m := by
-  by_cases n1 : n = 1 <;> [exact fun m2 _ => n1.symm ▸ le_trans (by simp) m2;
-    apply (minFac_has_prop n1).2.2]
+  by_cases n1 : n = 1
+  · exact fun m2 _ => n1.symm ▸ le_trans (by simp) m2
+  · apply (minFac_has_prop n1).2.2
 #align nat.min_fac_le_of_dvd Nat.minFac_le_of_dvd
 
 theorem minFac_pos (n : ℕ) : 0 < minFac n := by
-  by_cases n1 : n = 1 <;> [exact n1.symm ▸ (by simp); exact (minFac_prime n1).pos]
+  by_cases n1 : n = 1
+  · simp [n1]
+  · exact (minFac_prime n1).pos
 #align nat.min_fac_pos Nat.minFac_pos
 
 theorem minFac_le {n : ℕ} (H : 0 < n) : minFac n ≤ n :=

Mathlib/Data/Real/EReal.lean

@@ -1320,25 +1320,25 @@ lemma le_iff_le_forall_real_gt (x y : EReal) : (∀ z : ℝ, x < z → y ≤ z)
 
 lemma ge_iff_le_forall_real_lt (x y : EReal) : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h z z_lt_y ↦ le_trans (le_of_lt z_lt_y) h⟩
-  induction x
-  case h_bot =>
+  induction x with
+  | h_bot =>
     refine ((eq_bot_iff_forall_lt y).2 fun z ↦ ?_).le
     refine lt_of_not_le fun z_le_y ↦ (not_le_of_lt (bot_lt_coe (z - 1)) (h (z - 1)
       (lt_of_lt_of_le ?_ z_le_y)))
     exact_mod_cast sub_one_lt z
-  case h_real =>
-    induction y
-    case h_bot => exact bot_le
-    case h_real x y =>
+  | h_real x =>
+    induction y with
+    | h_bot => exact bot_le
+    | h_real y =>
       norm_cast at h ⊢
       by_contra! x_lt_y
       rcases exists_between x_lt_y with ⟨z, x_lt_z, z_lt_y⟩
       exact not_le_of_lt x_lt_z (h z z_lt_y)
-    case h_top x =>
+    | h_top =>
       exfalso
       norm_cast at h
       exact not_le_of_lt (lt_add_one x) <| h (x + 1) (coe_lt_top (x + 1))
-  case h_top => exact le_top
+  | h_top => exact le_top
 
 /-! ### Absolute value -/