chore: remove uses of cases' (#9171)

I literally went through and regex'd some uses of `cases'`, replacing them with `rcases`; this is meant to be a low effort PR as I hope that tools can do this in the future.

`rcases` is an easier replacement than `cases`, though with better tools we could in future do a second pass converting simple `rcases` added here (and existing ones) to `cases`.

Archive/Arithcc.lean

@@ -272,7 +272,7 @@ theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁
   constructor; · exact h.1
   intro r hr
   have hr : r ≤ t := Register.le_of_lt_succ hr
-  cases' lt_or_eq_of_le hr with hr hr
+  rcases lt_or_eq_of_le hr with hr | hr
   · cases' h with _ h
     specialize h r hr
     simp_all

Archive/Imo/Imo2011Q5.lean

@@ -24,7 +24,7 @@ open Int
 theorem imo2011_q5 (f : ℤ → ℤ) (hpos : ∀ n : ℤ, 0 < f n) (hdvd : ∀ m n : ℤ, f (m - n) ∣ f m - f n) :
     ∀ m n : ℤ, f m ≤ f n → f m ∣ f n := by
   intro m n h_fm_le_fn
-  cases' lt_or_eq_of_le h_fm_le_fn with h_fm_lt_fn h_fm_eq_fn
+  rcases lt_or_eq_of_le h_fm_le_fn with h_fm_lt_fn | h_fm_eq_fn
   · -- m < n
     let d := f m - f (m - n)
     have h_fn_dvd_d : f n ∣ d := by

Counterexamples/SeminormLatticeNotDistrib.lean

@@ -57,8 +57,8 @@ theorem not_distrib : ¬(p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ q1 ⊓ q2 := by
   apply c; nth_rw 1 [← eq_one]
   apply le_trans _ (le_sup_inf _)
   apply le_ciInf; intro x
-  cases' le_or_lt x.fst (1 / 3) with h1 h1
-  · cases' le_or_lt x.snd (2 / 3) with h2 h2
+  rcases le_or_lt x.fst (1 / 3) with h1 | h1
+  · rcases le_or_lt x.snd (2 / 3) with h2 | h2
     · calc
         4 / 3 = 4 * (1 - 2 / 3) := by norm_num
         _ ≤ 4 * (1 - x.snd) := (mul_le_mul_left zero_lt_four).mpr (sub_le_sub_left h2 _)

Counterexamples/SorgenfreyLine.lean

@@ -204,7 +204,7 @@ instance : T5Space ℝₗ := by
     (bUnion_mem_nhdsSet fun y hy => (isOpen_Ico y (Y y)).mem_nhds <| left_mem_Ico.2 (hY y hy))
   simp only [disjoint_iUnion_left, disjoint_iUnion_right, Ico_disjoint_Ico]
   intro y hy x hx
-  cases' le_total x y with hle hle
+  rcases le_total x y with hle | hle
   · calc
       min (X x) (Y y) ≤ X x := min_le_left _ _
       _ ≤ y := (not_lt.1 fun hyx => (hXd x hx).le_bot ⟨⟨hle, hyx⟩, subset_closure hy⟩)

Mathlib/Algebra/BigOperators/Ring.lean

@@ -227,7 +227,7 @@ variable {R : Type*} [CommRing R]
 theorem prod_range_cast_nat_sub (n k : ℕ) :
     ∏ i in range k, (n - i : R) = (∏ i in range k, (n - i) : ℕ) := by
   rw [prod_natCast]
-  cases' le_or_lt k n with hkn hnk
+  rcases le_or_lt k n with hkn | hnk
   · exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm
   · rw [← mem_range] at hnk
     rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -131,13 +131,13 @@ theorem stream_succ (h : Int.fract v ≠ 0) (n : ℕ) :
   induction' n with n ih
   · have H : (IntFractPair.of v).fr = Int.fract v := rfl
     rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]
-  · cases' eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone hsome
+  · rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome
     · rw [hnone] at ih
       rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
         succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
     · obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
       rw [hp] at ih
-      cases' eq_or_ne p.fr 0 with hz hnz
+      rcases eq_or_ne p.fr 0 with hz | hnz
       · rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
       · rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
 #align generalized_continued_fraction.int_fract_pair.stream_succ GeneralizedContinuedFraction.IntFractPair.stream_succ
@@ -298,11 +298,11 @@ variable {K} (v)
 that of the inverse of the fractional part of `v`.
 -/
 theorem of_s_succ (n : ℕ) : (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n := by
-  cases' eq_or_ne (fract v) 0 with h h
+  rcases eq_or_ne (fract v) 0 with h | h
   · obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
     rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int,
       Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]
-  cases' eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ h₁
+  rcases eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ | h₁
   · rwa [h₁, ← terminatedAt_iff_s_none,
       of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
       of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]
@@ -340,7 +340,7 @@ of an element `v` of `K` in terms of the convergents of the inverse of its fract
 -/
 theorem convergents'_succ :
     (of v).convergents' (n + 1) = ⌊v⌋ + 1 / (of (fract v)⁻¹).convergents' n := by
-  cases' eq_or_ne (fract v) 0 with h h
+  rcases eq_or_ne (fract v) 0 with h | h
   · obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
     rw [convergents'_of_int, fract_intCast, inv_zero, ← cast_zero, convergents'_of_int, cast_zero,
       div_zero, add_zero, floor_intCast]

Mathlib/Algebra/GeomSum.lean

@@ -208,7 +208,7 @@ theorem sub_one_dvd_pow_sub_one [Ring α] (x : α) (n : ℕ) :
   exact (Commute.one_right x).sub_dvd_pow_sub_pow n
 
 theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n := by
-  cases' le_or_lt y x with h h
+  rcases le_or_lt y x with h | h
   · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
     exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
   · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -449,7 +449,7 @@ section LinearOrderedAddCommGroup
 variable [LinearOrderedAddCommGroup α] {a b : α}
 
 theorem abs_nsmul (n : ℕ) (a : α) : |n • a| = n • |a| := by
-  cases' le_total a 0 with hneg hpos
+  rcases le_total a 0 with hneg | hpos
   · rw [abs_of_nonpos hneg, ← abs_neg, ← neg_nsmul, abs_of_nonneg]
     exact nsmul_nonneg (neg_nonneg.mpr hneg) n
   · rw [abs_of_nonneg hpos, abs_of_nonneg]
@@ -743,8 +743,8 @@ theorem pow_bit1_pos_iff : 0 < a ^ bit1 n ↔ 0 < a :=
 
 theorem strictMono_pow_bit1 (n : ℕ) : StrictMono fun a : R => a ^ bit1 n := by
   intro a b hab
-  cases' le_total a 0 with ha ha
-  · cases' le_or_lt b 0 with hb hb
+  rcases le_total a 0 with ha | ha
+  · rcases le_or_lt b 0 with hb | hb
     · rw [← neg_lt_neg_iff, ← neg_pow_bit1, ← neg_pow_bit1]
       exact pow_lt_pow_left (neg_lt_neg hab) (neg_nonneg.2 hb) n.bit1_ne_zero
     · exact (pow_bit1_nonpos_iff.2 ha).trans_lt (pow_bit1_pos_iff.2 hb)

Mathlib/Algebra/Homology/LocalCohomology.lean

@@ -250,7 +250,7 @@ instance ideal_powers_initial [hR : IsNoetherian R R] :
       apply Relation.ReflTransGen.single
       -- The inclusions `J^n1 ≤ J'` and `J^n2 ≤ J'` always form a triangle, based on
       -- which exponent is larger.
-      cases' le_total (unop j1.left) (unop j2.left) with h h
+      rcases le_total (unop j1.left) (unop j2.left) with h | h
       right; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
       left; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
 #align local_cohomology.ideal_powers_initial localCohomology.ideal_powers_initial

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -151,7 +151,7 @@ theorem eventually_iInf_lowerCentralSeries_eq [IsArtinian R M] :
   obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
     WellFounded.monotone_chain_condition.mp h_wf ⟨_, antitone_lowerCentralSeries R L M⟩
   refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
-  cases' le_or_lt l m with h h
+  rcases le_or_lt l m with h | h
   · rw [← hn _ hl, ← hn _ (hl.trans h)]
   · exact antitone_lowerCentralSeries R L M (le_of_lt h)
 

Mathlib/Algebra/Module/Torsion.lean

@@ -394,7 +394,7 @@ variable (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤)
 -- Porting note: mem_iSup_finset_iff_exists_sum now requires DecidableEq ι
 theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf [DecidableEq ι] :
     ⨆ i ∈ S, torsionBySet R M (p i) = torsionBySet R M ↑(⨅ i ∈ S, p i) := by
-  cases' S.eq_empty_or_nonempty with h h
+  rcases S.eq_empty_or_nonempty with h | h
   · simp only [h]
     -- Porting note: converts were not cooperating
     convert iSup_emptyset (f := fun i => torsionBySet R M (p i)) <;> simp

Mathlib/Algebra/Order/Field/Basic.lean

@@ -315,7 +315,7 @@ theorem inv_lt_one_iff_of_pos (h₀ : 0 < a) : a⁻¹ < 1 ↔ 1 < a :=
 #align inv_lt_one_iff_of_pos inv_lt_one_iff_of_pos
 
 theorem inv_lt_one_iff : a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a := by
-  cases' le_or_lt a 0 with ha ha
+  rcases le_or_lt a 0 with ha | ha
   · simp [ha, (inv_nonpos.2 ha).trans_lt zero_lt_one]
   · simp only [ha.not_le, false_or_iff, inv_lt_one_iff_of_pos ha]
 #align inv_lt_one_iff inv_lt_one_iff

Mathlib/Algebra/Order/Floor.lean

@@ -466,7 +466,7 @@ theorem floor_sub_nat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n :
     ⌊a - n⌋₊ = ⌊a⌋₊ - n := by
   obtain ha | ha := le_total a 0
   · rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
-  cases' le_total a n with h h
+  rcases le_total a n with h | h
   · rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
     exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)
   · rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_nat _, tsub_add_cancel_of_le h]
@@ -531,7 +531,7 @@ variable [LinearOrderedSemifield α] [FloorSemiring α]
 -- TODO: should these lemmas be `simp`? `norm_cast`?
 
 theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
-  cases' le_total a 0 with ha ha
+  rcases le_total a 0 with ha | ha
   · rw [floor_of_nonpos, floor_of_nonpos ha]
     · simp
     apply div_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg
@@ -1349,7 +1349,7 @@ theorem preimage_ceil_singleton (m : ℤ) : (ceil : α → ℤ) ⁻¹' {m} = Ioc
 #align int.preimage_ceil_singleton Int.preimage_ceil_singleton
 
 theorem fract_eq_zero_or_add_one_sub_ceil (a : α) : fract a = 0 ∨ fract a = a + 1 - (⌈a⌉ : α) := by
-  cases' eq_or_ne (fract a) 0 with ha ha
+  rcases eq_or_ne (fract a) 0 with ha | ha
   · exact Or.inl ha
   right
   suffices (⌈a⌉ : α) = ⌊a⌋ + 1 by

Mathlib/Algebra/Order/Group/Abs.lean

@@ -146,7 +146,7 @@ theorem abs_pos_of_neg (h : a < 0) : 0 < |a| :=
 #align abs_pos_of_neg abs_pos_of_neg
 
 theorem neg_abs_le_self (a : α) : -|a| ≤ a := by
-  cases' le_total 0 a with h h
+  rcases le_total 0 a with h | h
   · calc
       -|a| = -a := congr_arg Neg.neg (abs_of_nonneg h)
       _ ≤ 0 := neg_nonpos.mpr h
@@ -206,7 +206,7 @@ theorem lt_of_abs_lt (h : |a| < b) : a < b :=
 #align lt_of_abs_lt lt_of_abs_lt
 
 theorem max_sub_min_eq_abs' (a b : α) : max a b - min a b = |a - b| := by
-  cases' le_total a b with ab ba
+  rcases le_total a b with ab | ba
   · rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub]
     rwa [sub_nonpos]
   · rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg]

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -349,9 +349,9 @@ instance (priority := 100) CanonicallyLinearOrderedCommMonoid.semilatticeSup : S
 
 @[to_additive]
 theorem min_mul_distrib (a b c : α) : min a (b * c) = min a (min a b * min a c) := by
-  cases' le_total a b with hb hb
+  rcases le_total a b with hb | hb
   · simp [hb, le_mul_right]
-  · cases' le_total a c with hc hc
+  · rcases le_total a c with hc | hc
     · simp [hc, le_mul_left]
     · simp [hb, hc]
 #align min_mul_distrib min_mul_distrib

Mathlib/Algebra/Order/Monoid/MinMax.lean

@@ -23,7 +23,8 @@ variable {α β : Type*}
 
 @[to_additive]
 theorem fn_min_mul_fn_max [LinearOrder α] [CommSemigroup β] (f : α → β) (n m : α) :
-    f (min n m) * f (max n m) = f n * f m := by cases' le_total n m with h h <;> simp [h, mul_comm]
+    f (min n m) * f (max n m) = f n * f m := by
+  rcases le_total n m with h | h <;> simp [h, mul_comm]
 #align fn_min_mul_fn_max fn_min_mul_fn_max
 #align fn_min_add_fn_max fn_min_add_fn_max
 

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -32,7 +32,7 @@ theorem abs_two : |(2 : α)| = 2 :=
 
 theorem abs_mul (a b : α) : |a * b| = |a| * |b| := by
   rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
-  cases' le_total a 0 with ha ha <;> cases' le_total b 0 with hb hb <;>
+  rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
     simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul,
       mul_neg, neg_neg, *]
 #align abs_mul abs_mul

Mathlib/Algebra/Order/Sub/Canonical.lean

@@ -428,7 +428,7 @@ theorem tsub_pos_iff_lt : 0 < a - b ↔ b < a := by rw [tsub_pos_iff_not_le, not
 #align tsub_pos_iff_lt tsub_pos_iff_lt
 
 theorem tsub_eq_tsub_min (a b : α) : a - b = a - min a b := by
-  cases' le_total a b with h h
+  rcases le_total a b with h | h
   · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
   · rw [min_eq_right h]
 #align tsub_eq_tsub_min tsub_eq_tsub_min
@@ -497,7 +497,7 @@ end Contra
 
 
 theorem tsub_add_eq_max : a - b + b = max a b := by
-  cases' le_total a b with h h
+  rcases le_total a b with h | h
   · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
   · rw [max_eq_left h, tsub_add_cancel_of_le h]
 #align tsub_add_eq_max tsub_add_eq_max
@@ -506,7 +506,7 @@ theorem add_tsub_eq_max : a + (b - a) = max a b := by rw [add_comm, max_comm, ts
 #align add_tsub_eq_max add_tsub_eq_max
 
 theorem tsub_min : a - min a b = a - b := by
-  cases' le_total a b with h h
+  rcases le_total a b with h | h
   · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
   · rw [min_eq_right h]
 #align tsub_min tsub_min

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -863,7 +863,7 @@ private theorem toIxxMod_cyclic_left {x₁ x₂ x₃ : α} (h : toIcoMod hp x₁
   · obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2
     rw [hd, toIocMod_add_zsmul', toIcoMod_add_zsmul', add_le_add_iff_right]
     assumption -- Porting note: was `simpa`
-  cases' le_or_lt x₃' (x₁ + p) with h₃₁ h₁₃
+  rcases le_or_lt x₃' (x₁ + p) with h₃₁ | h₁₃
   · suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p
     · exact hIoc₂₁.symm.trans_ge h₃₁
     apply (toIocMod_eq_iff hp).2

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -99,7 +99,7 @@ theorem coeff_list_prod_of_natDegree_le (l : List S[X]) (n : ℕ) (hl : ∀ p 
       simpa using hl'
     have hdn : natDegree hd ≤ n := hl _ (List.mem_cons_self _ _)
     rcases hdn.eq_or_lt with (rfl | hdn')
-    · cases' h.eq_or_lt with h' h'
+    · rcases h.eq_or_lt with h' | h'
       · rw [← h', coeff_mul_degree_add_degree, leadingCoeff, leadingCoeff]
       · rw [coeff_eq_zero_of_natDegree_lt, coeff_eq_zero_of_natDegree_lt h', mul_zero]
         exact natDegree_mul_le.trans_lt (add_lt_add_left h' _)

Mathlib/Algebra/Tropical/Basic.lean

@@ -512,10 +512,10 @@ instance covariant_swap_mul [LE R] [Add R] [CovariantClass R R (Function.swap (
 
 instance covariant_add [LinearOrder R] : CovariantClass (Tropical R) (Tropical R) (· + ·) (· ≤ ·) :=
   ⟨fun x y z h => by
-    cases' le_total x y with hx hy
+    rcases le_total x y with hx | hy
     · rw [add_eq_left hx, add_eq_left (hx.trans h)]
     · rw [add_eq_right hy]
-      cases' le_total x z with hx hx
+      rcases le_total x z with hx | hx
       · rwa [add_eq_left hx]
       · rwa [add_eq_right hx]⟩
 #align tropical.covariant_add Tropical.covariant_add
@@ -543,7 +543,7 @@ instance instDistribTropical [LinearOrder R] [Add R] [CovariantClass R R (· + 
 theorem add_pow [LinearOrder R] [AddMonoid R] [CovariantClass R R (· + ·) (· ≤ ·)]
     [CovariantClass R R (Function.swap (· + ·)) (· ≤ ·)] (x y : Tropical R) (n : ℕ) :
     (x + y) ^ n = x ^ n + y ^ n := by
-  cases' le_total x y with h h
+  rcases le_total x y with h | h
   · rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]
   · rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]
 #align tropical.add_pow Tropical.add_pow

Mathlib/AlgebraicGeometry/Properties.lean

@@ -215,7 +215,7 @@ instance [h : IsIntegral X] : IsDomain (X.presheaf.obj (op ⊤)) :=
 instance (priority := 900) isReducedOfIsIntegral [IsIntegral X] : IsReduced X := by
   constructor
   intro U
-  cases' U.1.eq_empty_or_nonempty with h h
+  rcases U.1.eq_empty_or_nonempty with h | h
   · have : U = ⊥ := SetLike.ext' h
     haveI := CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty this)
     change _root_.IsReduced (X.sheaf.val.obj (op U))

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -642,7 +642,7 @@ theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (
     by_cases h : x < y
     · exact ⟨x, y, ⟨h₁, h⟩⟩
     · refine' ⟨y, x, ⟨h₁.symm, _⟩⟩
-      cases' lt_or_eq_of_le (not_lt.mp h) with h' h'
+      rcases lt_or_eq_of_le (not_lt.mp h) with h' | h'
       · exact h'
       · exfalso
         exact h₂ h'.symm

Mathlib/Analysis/Analytic/Basic.lean

@@ -928,7 +928,7 @@ theorem HasFPowerSeriesOnBall.sum (h : HasFPowerSeriesOnBall f p x r) {y : E}
 /-- The sum of a converging power series is continuous in its disk of convergence. -/
 protected theorem FormalMultilinearSeries.continuousOn [CompleteSpace F] :
     ContinuousOn p.sum (EMetric.ball 0 p.radius) := by
-  cases' (zero_le p.radius).eq_or_lt with h h
+  rcases (zero_le p.radius).eq_or_lt with h | h
   · simp [← h, continuousOn_empty]
   · exact (p.hasFPowerSeriesOnBall h).continuousOn
 #align formal_multilinear_series.continuous_on FormalMultilinearSeries.continuousOn

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -1709,7 +1709,7 @@ theorem IsLittleO.of_pow {f : α → 𝕜} {g : α → R} {n : ℕ} (h : (f ^ n)
 theorem IsBigOWith.inv_rev {f : α → 𝕜} {g : α → 𝕜'} (h : IsBigOWith c l f g)
     (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) : IsBigOWith c l (fun x => (g x)⁻¹) fun x => (f x)⁻¹ := by
   refine' IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => _))
-  cases' eq_or_ne (f x) 0 with hx hx
+  rcases eq_or_ne (f x) 0 with hx | hx
   · simp only [hx, h₀ hx, inv_zero, norm_zero, mul_zero, le_rfl]
   · have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
     replace hle := inv_le_inv_of_le (norm_pos_iff.2 hx) hle

Mathlib/Analysis/BoundedVariation.lean

@@ -107,7 +107,7 @@ theorem sum_le (f : α → E) {s : Set α} (n : ℕ) {u : ℕ → α} (hu : Mono
 theorem sum_le_of_monotoneOn_Icc (f : α → E) {s : Set α} {m n : ℕ} {u : ℕ → α}
     (hu : MonotoneOn u (Icc m n)) (us : ∀ i ∈ Icc m n, u i ∈ s) :
     (∑ i in Finset.Ico m n, edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s := by
-  cases' le_total n m with hnm hmn
+  rcases le_total n m with hnm | hmn
   · simp [Finset.Ico_eq_empty_of_le hnm]
   let π := projIcc m n hmn
   let v i := u (π i)

Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

@@ -184,7 +184,7 @@ theorem injOn_setOf_mem_Icc_setOf_lower_eq (x : ι → ℝ) :
     exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
   intro i
   simp only [Set.ext_iff, mem_setOf] at H
-  cases' (hx₁.1 i).eq_or_lt with hi₁ hi₁
+  rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁
   · have hi₂ : J₂.lower i = x i := (H _).1 hi₁
     have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
     have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i

Mathlib/Analysis/Calculus/Darboux.lean

@@ -78,7 +78,7 @@ theorem Set.OrdConnected.image_hasDerivWithinAt {s : Set ℝ} (hs : OrdConnected
     (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) : OrdConnected (f' '' s) := by
   apply ordConnected_of_Ioo
   rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ - m ⟨hma, hmb⟩
-  cases' le_total a b with hab hab
+  rcases le_total a b with hab | hab
   · have : Icc a b ⊆ s := hs.out ha hb
     rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma
         hmb with
@@ -154,4 +154,3 @@ theorem hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne {s : Set ℝ} (hs :
   exact (hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha)
     (mem_image_of_mem f' hb) ⟨hma, hmb⟩
 #align has_deriv_within_at_forall_lt_or_forall_gt_of_forall_ne hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne
-

Mathlib/Analysis/Calculus/Deriv/ZPow.lean

@@ -124,7 +124,7 @@ theorem iter_deriv_zpow (m : ℤ) (x : 𝕜) (k : ℕ) :
 theorem iter_deriv_pow (n : ℕ) (x : 𝕜) (k : ℕ) :
     deriv^[k] (fun x : 𝕜 => x ^ n) x = (∏ i in Finset.range k, ((n : 𝕜) - i)) * x ^ (n - k) := by
   simp only [← zpow_ofNat, iter_deriv_zpow, Int.cast_ofNat]
-  cases' le_or_lt k n with hkn hnk
+  rcases le_or_lt k n with hkn | hnk
   · rw [Int.ofNat_sub hkn]
   · have : (∏ i in Finset.range k, (n - i : 𝕜)) = 0 :=
       Finset.prod_eq_zero (Finset.mem_range.2 hnk) (sub_self _)

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

@@ -152,7 +152,7 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
     (f'symm : f'.NonlinearRightInverse) {ε : ℝ} {b : E} (ε0 : 0 ≤ ε) (hε : closedBall b ε ⊆ s) :
     SurjOn f (closedBall b ε) (closedBall (f b) (((f'symm.nnnorm : ℝ)⁻¹ - c) * ε)) := by
   intro y hy
-  cases' le_or_lt (f'symm.nnnorm : ℝ)⁻¹ c with hc hc
+  rcases le_or_lt (f'symm.nnnorm : ℝ)⁻¹ c with hc | hc
   · refine' ⟨b, by simp [ε0], _⟩
     have : dist y (f b) ≤ 0 :=
       (mem_closedBall.1 hy).trans (mul_nonpos_of_nonpos_of_nonneg (by linarith) ε0)