chore: tidy various files (#16132)

Author: Ruben-VandeVelde

Archive/Sensitivity.lean

@@ -279,10 +279,11 @@ is necessary since otherwise `n • v` refers to the multiplication defined
 using only the addition of `V`. -/
 
 
-theorem f_squared : ∀ v : V n, (f n) (f n v) = (n : ℝ) • v := by
-  induction' n with n IH _ <;> intro v
-  · simp only [Nat.cast_zero, zero_smul]; rfl
-  · cases v; rw [f_succ_apply, f_succ_apply]; simp [IH, add_smul (n : ℝ) 1, add_assoc, V]; abel
+theorem f_squared (v : V n) : (f n) (f n v) = (n : ℝ) • v := by
+  induction n with
+  | zero =>  simp only [Nat.cast_zero, zero_smul, f_zero, zero_apply]
+  | succ n IH =>
+    cases v; rw [f_succ_apply, f_succ_apply]; simp [IH, add_smul (n : ℝ) 1, add_assoc, V]; abel
 
 /-! We now compute the matrix of `f` in the `e` basis (`p` is the line index,
 `q` the column index). -/

Counterexamples/Phillips.lean

@@ -296,8 +296,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
     induction n with
     | zero =>
       simp only [s, BoundedAdditiveMeasure.empty, id, Nat.cast_zero, zero_mul,
-        Function.iterate_zero, Subtype.coe_mk]
-      rfl
+        Function.iterate_zero, Subtype.coe_mk, le_rfl]
     | succ n IH =>
       have : (s (n + 1)).1 = (s (n + 1)).1 \ (s n).1 ∪ (s n).1 := by
         simpa only [s, Function.iterate_succ', union_diff_self]

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -1527,11 +1527,11 @@ lemma prod_involution (g : ∀ a ∈ s, α) (hg₁ : ∀ a ha, f a * f (g a ha)
   have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]
   suffices h : ∏ x ∈ s \ {x, g x hx}, f x = 1 by
     rw [← prod_sdiff this, h, one_mul]
-    rcases eq_or_ne (g x hx) x
-    case inl hx' => simpa [hx'] using hg₃ x hx
-    case inr hx' => rw [prod_pair hx'.symm, hg₁]
-  suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} by
-    exact ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _
+    cases eq_or_ne (g x hx) x with
+    | inl hx' => simpa [hx'] using hg₃ x hx
+    | inr hx' => rw [prod_pair hx'.symm, hg₁]
+  suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} from
+    ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _
       (by simp [hg₁]) (fun _ _ => hg₃ _ _) h₃ (fun _ _ => hg₄ _ _)
   simp only [mem_sdiff, mem_insert, mem_singleton, not_or, g_mem, true_and]
   rintro a ⟨ha₁, ha₂, ha₃⟩

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

@@ -99,29 +99,28 @@ theorem compExactValue_correctness_of_stream_eq_some :
   induction n with
   | zero =>
     intro ifp_zero stream_zero_eq
-    -- Nat.zero
-    have : IntFractPair.of v = ifp_zero := by
+    obtain rfl : IntFractPair.of v = ifp_zero := by
       have : IntFractPair.stream v 0 = some (IntFractPair.of v) := rfl
       simpa only [this, Option.some.injEq] using stream_zero_eq
-    cases this
-    cases' Decidable.em (Int.fract v = 0) with fract_eq_zero fract_ne_zero
-    -- Int.fract v = 0; we must then have `v = ⌊v⌋`
-    · suffices v = ⌊v⌋ by
+    cases eq_or_ne (Int.fract v) 0 with
+    | inl fract_eq_zero =>
+      -- Int.fract v = 0; we must then have `v = ⌊v⌋`
+      suffices v = ⌊v⌋ by
         -- Porting note: was `simpa [contsAux, fract_eq_zero, compExactValue]`
         field_simp [nextConts, nextNum, nextDen, compExactValue]
         have : (IntFractPair.of v).fr = Int.fract v := rfl
         rwa [this, if_pos fract_eq_zero]
       calc
         v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
         _ = ⌊v⌋ := by simp [fract_eq_zero]
-    -- Int.fract v ≠ 0; the claim then easily follows by unfolding a single computation step
-    · field_simp [contsAux, nextConts, nextNum, nextDen, of_h_eq_floor, compExactValue]
+    | inr fract_ne_zero =>
+      -- Int.fract v ≠ 0; the claim then easily follows by unfolding a single computation step
+      field_simp [contsAux, nextConts, nextNum, nextDen, of_h_eq_floor, compExactValue]
       -- Porting note: this and the if_neg rewrite are needed
       have : (IntFractPair.of v).fr = Int.fract v := rfl
       rw [this, if_neg fract_ne_zero, Int.floor_add_fract]
   | succ n IH =>
     intro ifp_succ_n succ_nth_stream_eq
-    -- Nat.succ
     obtain ⟨ifp_n, nth_stream_eq, nth_fract_ne_zero, -⟩ :
       ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
         ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
@@ -130,9 +129,10 @@ theorem compExactValue_correctness_of_stream_eq_some :
     let conts := g.contsAux (n + 2)
     set pconts := g.contsAux (n + 1) with pconts_eq
     set ppconts := g.contsAux n with ppconts_eq
-    cases' Decidable.em (ifp_succ_n.fr = 0) with ifp_succ_n_fr_eq_zero ifp_succ_n_fr_ne_zero
-    -- ifp_succ_n.fr = 0
-    · suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
+    cases eq_or_ne ifp_succ_n.fr 0 with
+    | inl ifp_succ_n_fr_eq_zero =>
+      -- ifp_succ_n.fr = 0
+      suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
       -- use the IH and the fact that ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ to prove this case
       obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor⟩ :
           ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
@@ -145,8 +145,9 @@ theorem compExactValue_correctness_of_stream_eq_some :
       suffices v = compExactValue ppconts pconts ifp_n.fr by
         simpa [conts, contsAux, s_nth_eq, compExactValue, nth_fract_ne_zero] using this
       exact IH nth_stream_eq
-    -- ifp_succ_n.fr ≠ 0
-    · -- use the IH to show that the following equality suffices
+    | inr ifp_succ_n_fr_ne_zero =>
+      -- ifp_succ_n.fr ≠ 0
+      -- use the IH to show that the following equality suffices
       suffices
         compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr by
         have : v = compExactValue ppconts pconts ifp_n.fr := IH nth_stream_eq
@@ -214,14 +215,14 @@ theorem of_correctness_of_nth_stream_eq_none (nth_stream_eq_none : IntFractPair.
   | succ n IH =>
     let g := of v
     change v = g.convs n
-    have :
+    obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
       IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
       IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none
-    rcases this with (⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩)
-    · cases' n with n'
-      · contradiction
-      -- IntFractPair.stream v 0 ≠ none
-      · have : g.TerminatedAt n' :=
+    · cases n with
+      | zero => contradiction
+      | succ n' =>
+        -- IntFractPair.stream v 0 ≠ none
+        have : g.TerminatedAt n' :=
           of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
             nth_stream_eq_none
         have : g.convs (n' + 1) = g.convs n' :=

Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean

@@ -62,7 +62,7 @@ def homotopyPInftyToId : Homotopy (PInfty : K[X] ⟶ _) (𝟙 _) where
     · simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex,
         PInfty_f, P_f_0_eq, zero_add] using (homotopyPToId X 2).comm 0
     · simp only [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex,
-        HomologicalComplex.id_f, PInfty_f, ← P_is_eventually_constant (rfl.le : n + 1 ≤ n + 1)]
+        HomologicalComplex.id_f, PInfty_f, ← P_is_eventually_constant (le_refl <| n + 1)]
       -- Porting note(lean4/2146): remaining proof was
       -- `simpa only [homotopyPToId_eventually_constant X (lt_add_one (Nat.succ n))]
       -- using (homotopyPToId X (n + 2)).comm (n + 1)`;

Mathlib/AlgebraicTopology/DoldKan/PInfty.lean

@@ -33,10 +33,11 @@ variable {C : Type*} [Category C] [Preadditive C] {X : SimplicialObject C}
 
 theorem P_is_eventually_constant {q n : ℕ} (hqn : n ≤ q) :
     ((P (q + 1)).f n : X _[n] ⟶ _) = (P q).f n := by
-  rcases n with (_|n)
-  · simp only [P_f_0_eq]
-  · simp only [P_succ, add_right_eq_self, comp_add, HomologicalComplex.comp_f,
-      HomologicalComplex.add_f_apply, comp_id]
+  cases n with
+  | zero => simp only [P_f_0_eq]
+  | succ n =>
+    simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
+      add_right_eq_self]
     exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)
 
 theorem Q_is_eventually_constant {q n : ℕ} (hqn : n ≤ q) :

Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

@@ -54,7 +54,7 @@ def connectedComponents : Cat.{v, u} ⥤ Type u where
   obj C := ConnectedComponents C
   map F := Functor.mapConnectedComponents F
   map_id _ := funext fun x ↦ (Quotient.exists_rep x).elim (fun _ h ↦ by subst h; rfl)
-  map_comp _ _ := funext fun x ↦ (Quotient.exists_rep x).elim (fun _ h => by subst h;rfl)
+  map_comp _ _ := funext fun x ↦ (Quotient.exists_rep x).elim (fun _ h => by subst h; rfl)
 
 /-- `typeToCat : Type ⥤ Cat` is right adjoint to `connectedComponents : Cat ⥤ Type` -/
 def connectedComponentsTypeToCatAdj : connectedComponents ⊣ typeToCat where

Mathlib/Combinatorics/SimpleGraph/Diam.lean

@@ -190,13 +190,11 @@ lemma diam_top [Nontrivial α] : (⊤ : SimpleGraph α).diam = 1 := by
 
 @[simp]
 lemma diam_eq_zero : G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α := by
-  rw [diam, ENat.toNat_eq_zero]
-  aesop
+  rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]
 
 @[simp]
 lemma diam_eq_one [Nontrivial α] : G.diam = 1 ↔ G = ⊤ := by
-  rw [diam, ENat.toNat_eq_iff (by decide)]
-  exact ediam_eq_one
+  rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]
 
 end diam
 

Mathlib/Data/Finset/Lattice.lean

@@ -18,7 +18,6 @@ import Mathlib.Order.Nat
 # Lattice operations on finsets
 -/
 
--- TODO:
 assert_not_exists OrderedCommMonoid
 assert_not_exists MonoidWithZero
 

Mathlib/Data/List/Sort.lean

@@ -256,7 +256,7 @@ theorem perm_insertionSort : ∀ l : List α, insertionSort r l ~ l
     simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)
 
 @[simp]
-theorem mem_insertionSort  {l : List α} {x : α} : x ∈ l.insertionSort r ↔ x ∈ l :=
+theorem mem_insertionSort {l : List α} {x : α} : x ∈ l.insertionSort r ↔ x ∈ l :=
   (perm_insertionSort r l).mem_iff
 
 @[simp]