chore: automatically replace cases' used to split Or (leanprover-community#16526)

Let `h : Or a b`. We replace `cases' h with ha hb` with `rcases h with ha | hb`.

To get all uses of `cases'` apply the following diff and run `lake build -q > cases-targets`:
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 34ad80c..944d54b992c 100644

Author: Parcly-Taxel

Mathlib/Algebra/Group/Int/Even.lean

@@ -22,13 +22,13 @@ namespace Int
 variable {m n : ℤ}
 
 @[simp] lemma emod_two_ne_one : ¬n % 2 = 1 ↔ n % 2 = 0 := by
-  cases' emod_two_eq_zero_or_one n with h h <;> simp [h]
+  rcases emod_two_eq_zero_or_one n with h | h <;> simp [h]
 
 @[simp] lemma one_emod_two : (1 : Int) % 2 = 1 := rfl
 
 -- `EuclideanDomain.mod_eq_zero` uses (2 ∣ n) as normal form
 @[local simp] lemma emod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by
-  cases' emod_two_eq_zero_or_one n with h h <;> simp [h]
+  rcases emod_two_eq_zero_or_one n with h | h <;> simp [h]
 
 lemma even_iff : Even n ↔ n % 2 = 0 where
   mp := fun ⟨m, hm⟩ ↦ by simp [← Int.two_mul, hm]
@@ -49,8 +49,8 @@ instance : DecidablePred (IsSquare : ℤ → Prop) :=
 @[simp] lemma not_even_one : ¬Even (1 : ℤ) := by simp [even_iff]
 
 @[parity_simps] lemma even_add : Even (m + n) ↔ (Even m ↔ Even n) := by
-  cases' emod_two_eq_zero_or_one m with h₁ h₁ <;>
-  cases' emod_two_eq_zero_or_one n with h₂ h₂ <;>
+  rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
+  rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
   simp [even_iff, h₁, h₂, Int.add_emod, one_add_one_eq_two, emod_self]
 
 lemma two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1 := by simp [add_emod]
@@ -63,8 +63,8 @@ lemma even_sub : Even (m - n) ↔ (Even m ↔ Even n) := by simp [sub_eq_add_neg
 @[parity_simps] lemma even_sub_one : Even (n - 1) ↔ ¬Even n := by simp [even_sub]
 
 @[parity_simps] lemma even_mul : Even (m * n) ↔ Even m ∨ Even n := by
-  cases' emod_two_eq_zero_or_one m with h₁ h₁ <;>
-  cases' emod_two_eq_zero_or_one n with h₂ h₂ <;>
+  rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
+  rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
   simp [even_iff, h₁, h₂, Int.mul_emod]
 
 @[parity_simps] lemma even_pow {n : ℕ} : Even (m ^ n) ↔ Even m ∧ n ≠ 0 := by

Mathlib/Algebra/Homology/AlternatingConst.lean

@@ -58,7 +58,7 @@ def alternatingConstHomologyDataZero (X : C) (n : ℕ) (hn : n = 0) :
   .ofZeros _ (by simp [hn]) (by simp [hn])
 
 instance (X : C) (n : ℕ) : (alternatingConst.obj X).HasHomology n := by
-  cases' n.even_or_odd with h h
+  rcases n.even_or_odd with h | h
   · cases' n with n
     · exact ⟨⟨alternatingConstHomologyDataZero X _ rfl⟩⟩
     · exact ⟨⟨alternatingConstHomologyDataEvenNEZero X _ h (by simp)⟩⟩
@@ -67,7 +67,7 @@ instance (X : C) (n : ℕ) : (alternatingConst.obj X).HasHomology n := by
 /-- The `n`-th homology of the alternating constant complex is `X` for `n ≠ 0`. -/
 lemma alternatingConst_exactAt (X : C) (n : ℕ) (hn : n ≠ 0) :
     (alternatingConst.obj X).ExactAt n := by
-  cases' n.even_or_odd with h h
+  rcases n.even_or_odd with h | h
   · exact ⟨(alternatingConstHomologyDataEvenNEZero X _ h hn), isZero_zero C⟩
   · exact ⟨(alternatingConstHomologyDataOdd X _ h), isZero_zero C⟩
 

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -407,7 +407,7 @@ theorem nilpotencyLength_eq_one_iff [Nontrivial M] :
 theorem isTrivial_of_nilpotencyLength_le_one [IsNilpotent L M] (h : nilpotencyLength L M ≤ 1) :
     IsTrivial L M := by
   nontriviality M
-  cases' Nat.le_one_iff_eq_zero_or_eq_one.mp h with h h
+  rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h with h | h
   · rw [nilpotencyLength_eq_zero_iff] at h; infer_instance
   · rwa [nilpotencyLength_eq_one_iff] at h
 

Mathlib/Algebra/Lie/Solvable.lean

@@ -85,7 +85,7 @@ theorem derivedSeriesOfIdeal_le {I J : LieIdeal R L} {k l : ℕ} (h₁ : I ≤ J
   revert l; induction' k with k ih <;> intro l h₂
   · rw [le_zero_iff] at h₂; rw [h₂, derivedSeriesOfIdeal_zero]; exact h₁
   · have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
-    cases' h with h h
+    rcases h with h | h
     · rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
       exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))
     · rw [derivedSeriesOfIdeal_succ]; exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -136,7 +136,7 @@ protected theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*)
   -- Eliminate the binomial coefficients from the picture.
   suffices (f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ m₂) = 0 by rw [this]; apply smul_zero
   -- Finish off with appropriate case analysis.
-  cases' Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi hj
+  rcases Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi | hj
   · rw [(hf_comm.pow_pow i j).eq, LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hi hf₁,
       LinearMap.map_zero]
   · rw [LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hj hf₂, LinearMap.map_zero]

Mathlib/Algebra/Module/Torsion.lean

@@ -760,7 +760,7 @@ theorem noZeroSMulDivisors_iff_torsion_eq_bot : NoZeroSMulDivisors R M ↔ torsi
     rw [eq_bot_iff]
     rintro x ⟨a, hax⟩
     change (a : R) • x = 0 at hax
-    cases' eq_zero_or_eq_zero_of_smul_eq_zero hax with h0 h0
+    rcases eq_zero_or_eq_zero_of_smul_eq_zero hax with h0 | h0
     · exfalso
       exact nonZeroDivisors.coe_ne_zero a h0
     · exact h0

Mathlib/Algebra/MvPolynomial/CommRing.lean

@@ -183,7 +183,7 @@ theorem degreeOf_sub_lt {x : σ} {f g : MvPolynomial σ R} {k : ℕ} (h : 0 < k)
   by_contra! hc
   have h := support_sub σ f g hm
   simp only [mem_support_iff, Ne, coeff_sub, sub_eq_zero] at hm
-  cases' Finset.mem_union.1 h with cf cg
+  rcases Finset.mem_union.1 h with cf | cg
   · exact hm (hf m cf hc)
   · exact hm (hg m cg hc)
 

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -188,7 +188,7 @@ variable [OrderedCommMonoid M] [CanonicallyOrderedMul M] {l : List M}
 
 @[to_additive] lemma monotone_prod_take (L : List M) : Monotone fun i => (L.take i).prod := by
   refine monotone_nat_of_le_succ fun n => ?_
-  cases' lt_or_le n L.length with h h
+  rcases lt_or_le n L.length with h | h
   · rw [prod_take_succ _ _ h]
     exact le_self_mul
   · simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

Mathlib/Algebra/Order/CauSeq/Basic.lean

@@ -604,7 +604,7 @@ protected theorem mul_pos {f g : CauSeq α abs} : Pos f → Pos g → Pos (f * g
       mul_le_mul h₁ h₂ (le_of_lt G0) (le_trans (le_of_lt F0) h₁)⟩
 
 theorem trichotomy (f : CauSeq α abs) : Pos f ∨ LimZero f ∨ Pos (-f) := by
-  cases' Classical.em (LimZero f) with h h <;> simp [*]
+  rcases Classical.em (LimZero f) with h | h <;> simp [*]
   rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
   rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
   refine (le_total 0 (f i)).imp ?_ ?_ <;>

Mathlib/Algebra/Order/Field/Power.lean

@@ -125,7 +125,7 @@ alias ⟨_, Odd.zpow_neg⟩ := Odd.zpow_neg_iff
 alias ⟨_, Odd.zpow_nonpos⟩ := Odd.zpow_nonpos_iff
 
 theorem Even.zpow_abs {p : ℤ} (hp : Even p) (a : α) : |a| ^ p = a ^ p := by
-  cases' abs_choice a with h h <;> simp only [h, hp.neg_zpow _]
+  rcases abs_choice a with h | h <;> simp only [h, hp.neg_zpow _]
 
 /-! ### Bernoulli's inequality -/