chore: replace single-subgoal cases' (leanprover-community#21976)

Replace uses of `cases'` that generate only one subgoal with `obtain` (or `rcases` if it is of the form `cases' h : f x`).

```python
#!/usr/bin/env python3
import re
keys = {}

with open("cases-uses", 'r') as f:
    for l in f:
        filename, line_n, col_n, rest = l.split(':', maxsplit=3)
        i = int(line_n)-1
        col_n = int(col_n)
        head, sep, n_subgoals = rest.strip().rpartition(' ')
        n_subgoals = int(n_subgoals)
        assert head.endswith(']')
        head, sep, newvars = head[:-1].rpartition(' [')
        assert sep
        newvars = newvars.split(', ')
        if filename not in keys:
            keys[filename] = {}
        if i not in keys[filename]:
            keys[filename][i] = {}
        keys[filename][i].update({col_n: (head, newvars, n_subgoals)})

for (filename, d) in keys.items():
    with open(filename, 'r') as f:
        lines = f.readlines()
    for (i, t) in d.items():
        line = lines[i]
        for (col_n, (head, newvars, n_subgoals)) in t.items():
            cases_re = re.compile(rf"cases' (.*?) with " + " ".join(newvars))
            def rf(m):
                if n_subgoals == 1:
                    if ':' not in m[1]:
                        return f"obtain ⟨{', '.join(newvars)}⟩ := {m[1]}"
                    return f"rcases {m[1]} with ⟨{', '.join(newvars)}⟩"
                return m[0]
            line = cases_re.sub(rf, line, 1)
        lines[i] = line
    with open(filename, 'w') as f:
        f.write("".join(lines))
```

The version of `cases-uses` used for this replacement was extracted from [this run](https://github.com/leanprover-community/mathlib4/actions/runs/13362153558/job/37313542212) and is available [here](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/The.20plan.20to.20remove.20cases'/near/500097792).

Author: Parcly-Taxel

Archive/Imo/Imo2008Q3.lean

@@ -48,7 +48,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hnat₃ : p ≥ 2 * n := by omega
   set k : ℕ := p - 2 * n with hnat₄
   have hnat₅ : p ∣ k ^ 2 + 4 := by
-    cases' hnat₁ with x hx
+    obtain ⟨x, hx⟩ := hnat₁
     have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
       use (p : ℤ) - 4 * n + 4 * x
       have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast

Archive/MiuLanguage/DecisionNec.lean

@@ -122,7 +122,7 @@ We'll show, for each `i` from 1 to 4, that if `en` follows by Rule `i` from `st`
 
 theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ [I])) (h₂ : Goodm (xs ++ [I])) :
     Goodm (xs ++ [I, U]) := by
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   constructor
   · cases xs <;> simp_all
   · change ¬M ∈ tail (xs ++ ([I] ++ [U]))
@@ -134,14 +134,14 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
     Goodm ((M :: xs) ++ xs) := by
   constructor
   · rfl
-  · cases' h₂ with mhead mtail
+  · obtain ⟨mhead, mtail⟩ := h₂
     contrapose! mtail
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
 theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs))
     (h₂ : Goodm (as ++ [I, I, I] ++ bs)) : Goodm (as ++ (U :: bs)) := by
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
   · cases as
@@ -159,7 +159,7 @@ The proof of the next lemma is identical, on the tactic level, to the previous p
 
 theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
     (h₂ : Goodm (as ++ [U, U] ++ bs)) : Goodm (as ++ bs) := by
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
   · cases as

Archive/Sensitivity.lean

@@ -210,7 +210,7 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
 theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by
   induction' n with n ih
   · dsimp [ε] at h; exact h fun _ => true
-  · cases' v with v₁ v₂
+  · obtain ⟨v₁, v₂⟩ := v
     ext <;> change _ = (0 : V n) <;> simp only <;> apply ih <;> intro p <;>
       [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred h);
       let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred h)]

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -56,7 +56,7 @@ theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).Pr
 
 theorem eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) : ∃ k m : ℕ, n = 2 ^ k * m ∧ ¬Even m := by
   have h := Nat.finiteMultiplicity_iff.2 ⟨Nat.prime_two.ne_one, hpos⟩
-  cases' pow_multiplicity_dvd 2 n with m hm
+  obtain ⟨m, hm⟩ := pow_multiplicity_dvd 2 n
   use multiplicity 2 n, m
   refine ⟨hm, ?_⟩
   rw [even_iff_two_dvd]

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -226,7 +226,7 @@ lemma genWeightSpace_ne_bot (χ : Weight R L M) : genWeightSpace M χ ≠ ⊥ :=
 variable {M}
 
 @[ext] lemma ext {χ₁ χ₂ : Weight R L M} (h : ∀ x, χ₁ x = χ₂ x) : χ₁ = χ₂ := by
-  cases' χ₁ with f₁ _; cases' χ₂ with f₂ _; aesop
+  obtain ⟨f₁, _⟩ := χ₁; obtain ⟨f₂, _⟩ := χ₂; aesop
 
 lemma ext_iff' {χ₁ χ₂ : Weight R L M} : (χ₁ : L → R) = χ₂ ↔ χ₁ = χ₂ := by simp
 

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -217,7 +217,7 @@ theorem coeff_multiset_prod_of_natDegree_le (n : ℕ) (hl : ∀ p ∈ t, natDegr
 
 theorem coeff_prod_of_natDegree_le (f : ι → R[X]) (n : ℕ) (h : ∀ p ∈ s, natDegree (f p) ≤ n) :
     coeff (∏ i ∈ s, f i) (#s * n) = ∏ i ∈ s, coeff (f i) n := by
-  cases' s with l hl
+  obtain ⟨l, hl⟩ := s
   convert coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
   · simp
   · simp

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -446,12 +446,12 @@ theorem eval_gcd_eq_zero [DecidableEq R] {f g : R[X]} {α : R}
 
 theorem root_left_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
     (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : f.eval₂ ϕ α = 0 := by
-  cases' EuclideanDomain.gcd_dvd_left f g with p hp
+  obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g
   rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
 
 theorem root_right_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
     (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : g.eval₂ ϕ α = 0 := by
-  cases' EuclideanDomain.gcd_dvd_right f g with p hp
+  obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g
   rw [hp, Polynomial.eval₂_mul, hα, zero_mul]
 
 theorem root_gcd_iff_root_left_right [CommSemiring k] [DecidableEq R]

Mathlib/Analysis/Analytic/Composition.lean

@@ -117,7 +117,7 @@ theorem applyComposition_single (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
   dsimp
   congr 1
   convert Composition.single_embedding hn ⟨i, hi2⟩ using 1
-  cases' j with j_val j_property
+  obtain ⟨j_val, j_property⟩ := j
   have : j_val = 0 := le_bot_iff.1 (Nat.lt_succ_iff.1 j_property)
   congr!
   simp

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -288,7 +288,7 @@ theorem mk'_eq_bot {l u : ι → ℝ} : mk' l u = ⊥ ↔ ∃ i, u i ≤ l i :=
 
 @[simp]
 theorem mk'_eq_coe {l u : ι → ℝ} : mk' l u = I ↔ l = I.lower ∧ u = I.upper := by
-  cases' I with lI uI hI; rw [mk']; split_ifs with h
+  obtain ⟨lI, uI, hI⟩ := I; rw [mk']; split_ifs with h
   · simp [WithBot.coe_eq_coe]
   · suffices l = lI → u ≠ uI by simpa
     rintro rfl rfl

Mathlib/Analysis/Calculus/Taylor.lean

@@ -120,10 +120,8 @@ theorem continuousOn_taylorWithinEval {f : ℝ → E} {x : ℝ} {n : ℕ} {s : S
   refine continuousOn_finset_sum (Finset.range (n + 1)) fun i hi => ?_
   refine (continuousOn_const.mul ((continuousOn_const.sub continuousOn_id).pow _)).smul ?_
   rw [contDiffOn_nat_iff_continuousOn_differentiableOn_deriv hs] at hf
-  cases' hf with hf_left
-  specialize hf_left i
   simp only [Finset.mem_range] at hi
-  refine hf_left ?_
+  refine hf.1 i ?_
   simp only [WithTop.coe_le_coe, Nat.cast_le, Nat.lt_succ_iff.mp hi]
 
 /-- Helper lemma for calculating the derivative of the monomial that appears in Taylor