style: use cases x with | ... instead of cases x; case => ... (#9321

)

This converts usages of the pattern
```lean
cases h
case inl h' => ...
case inr h' => ...
```
which derive from mathported code, to the "structured `cases`" syntax:
```lean
cases h with
| inl h' => ...
| inr h' => ...
```
The case where the subgoals are handled with `·` instead of `case` is more contentious (and much more numerous) so I left those alone. This pattern also appears with `cases'`, `induction`, `induction'`, and `rcases`. Furthermore, there is a similar transformation for `by_cases`:
```lean
by_cases h : cond
case pos => ...
case neg => ...
```
is replaced by:
```lean
if h : cond then
  ...
else
  ...
```



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Archive/Arithcc.lean

@@ -303,23 +303,21 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
 
 Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit.
 -/
-theorem compiler_correctness :
-    ∀ (map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register),
-      (∀ x, read (loc x map) η = ξ x) →
-        (∀ x, loc x map < t) → outcome (compile map e t) η ≃[t] { η with ac := value e ξ } := by
-  intro map e ξ η t hmap ht
-  revert η t
-  induction e <;> intro η t hmap ht
+theorem compiler_correctness
+    (map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register)
+    (hmap : ∀ x, read (loc x map) η = ξ x) (ht : ∀ x, loc x map < t) :
+    outcome (compile map e t) η ≃[t] { η with ac := value e ξ } := by
+  induction e generalizing η t with
   -- 5.I
-  case const => simp [StateEq, step]; rfl
+  | const => simp [StateEq, step]; rfl
   -- 5.II
-  case var =>
+  | var =>
     simp [hmap, StateEq, step] -- Porting note: was `finish [hmap, StateEq, step]`
     constructor
     · simp_all only [read, loc]
     · rfl
   -- 5.III
-  case sum =>
+  | sum =>
     rename_i e_s₁ e_s₂ e_ih_s₁ e_ih_s₂
     simp
     generalize value e_s₁ ξ = ν₁ at e_ih_s₁ ⊢

Archive/Imo/Imo1962Q1.lean

@@ -145,11 +145,11 @@ theorem satisfied_by_153846 : ProblemPredicate 153846 := by
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 
 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by
-  cases' without_digits h1 with c h2
+  have ⟨c, h2⟩ := without_digits h1
   have h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6 := by apply lt_or_ge
-  cases' h3 with h3 h3
-  case inr => exact case_more_digits h3 h2
-  case inl =>
+  cases h3 with
+  | inr h3 => exact case_more_digits h3 h2
+  | inl h3 =>
     interval_cases h : (digits 10 c).length
     · exfalso; exact case_0_digit h h2
     · exfalso; exact case_1_digit h h2

Mathlib/Algebra/Associated.lean

@@ -1143,25 +1143,23 @@ theorem one_or_eq_of_le_of_prime : ∀ p m : Associates α, Prime p → m ≤ p
     rw [r]
     match h m d dvd_rfl' with
     | Or.inl h' =>
-      by_cases h : m = 0
-      case pos =>
+      if h : m = 0 then
         simp [h, zero_mul]
-      case neg =>
+      else
         rw [r] at h'
         have : m * d ≤ m * 1 := by simpa using h'
         have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
         have : d = 1 := bot_unique this
         simp [this]
     | Or.inr h' =>
-        by_cases h : d = 0
-        case pos =>
-          rw [r] at hp0
-          have : m * d = 0 := by rw [h]; simp
-          contradiction
-        case neg =>
-          rw [r] at h'
-          have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
-          exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
+      if h : d = 0 then
+        rw [r] at hp0
+        have : m * d = 0 := by rw [h]; simp
+        contradiction
+      else
+        rw [r] at h'
+        have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
+        exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
 #align associates.one_or_eq_of_le_of_prime Associates.one_or_eq_of_le_of_prime
 
 instance : CanonicallyOrderedCommMonoid (Associates α) where

Mathlib/Algebra/CharP/ExpChar.lean

@@ -102,9 +102,9 @@ theorem char_prime_of_ne_zero {p : ℕ} [hp : CharP R p] (p_ne_zero : p ≠ 0) :
 
 /-- The exponential characteristic is a prime number or one. -/
 theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 := by
-  cases hq
-  case zero => exact .inr rfl
-  case prime hp _ => exact .inl hp
+  cases hq with
+  | zero => exact .inr rfl
+  | prime hp => exact .inl hp
 #align exp_char_is_prime_or_one expChar_is_prime_or_one
 
 /-- The exponential characteristic is positive. -/

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -68,12 +68,12 @@ of great interest for the end user.
 /-- Shows that the fractional parts of the stream are in `[0,1)`. -/
 theorem nth_stream_fr_nonneg_lt_one {ifp_n : IntFractPair K}
     (nth_stream_eq : IntFractPair.stream v n = some ifp_n) : 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1 := by
-  cases n
-  case zero =>
+  cases n with
+  | zero =>
     have : IntFractPair.of v = ifp_n := by injection nth_stream_eq
     rw [← this, IntFractPair.of]
     exact ⟨fract_nonneg _, fract_lt_one _⟩
-  case succ =>
+  | succ =>
     rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩
     rw [← ifp_of_eq_ifp_n, IntFractPair.of]
     exact ⟨fract_nonneg _, fract_lt_one _⟩
@@ -238,9 +238,9 @@ theorem succ_nth_fib_le_of_nth_denom (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n -
     (fib (n + 1) : K) ≤ (of v).denominators n := by
   rw [denom_eq_conts_b, nth_cont_eq_succ_nth_cont_aux]
   have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by
-    cases' n with n
-    case zero => exact Or.inl <| le_refl 1
-    case succ => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)
+    cases n with
+    | zero => exact Or.inl <| le_refl 1
+    | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)
   exact fib_le_of_continuantsAux_b this
 #align generalized_continued_fraction.succ_nth_fib_le_of_nth_denom GeneralizedContinuedFraction.succ_nth_fib_le_of_nth_denom
 
@@ -249,9 +249,9 @@ theorem succ_nth_fib_le_of_nth_denom (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n -
 
 theorem zero_le_of_continuantsAux_b : 0 ≤ ((of v).continuantsAux n).b := by
   let g := of v
-  induction' n with n IH
-  case zero => rfl
-  case succ =>
+  induction n with
+  | zero => rfl
+  | succ n IH =>
     cases' Decidable.em <| g.TerminatedAt (n - 1) with terminated not_terminated
     · -- terminating case
       cases' n with n
@@ -320,9 +320,9 @@ Next we prove the so-called *determinant formula* for `GeneralizedContinuedFract
 theorem determinant_aux (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)) :
     ((of v).continuantsAux n).a * ((of v).continuantsAux (n + 1)).b -
       ((of v).continuantsAux n).b * ((of v).continuantsAux (n + 1)).a = (-1) ^ n := by
-  induction' n with n IH
-  case zero => simp [continuantsAux]
-  case succ =>
+  induction n with
+  | zero => simp [continuantsAux]
+  | succ n IH =>
     -- set up some shorthand notation
     let g := of v
     let conts := continuantsAux g (n + 2)

Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -175,16 +175,16 @@ theorem coe_of_rat_eq : ((IntFractPair.of q).mapFr (↑) : IntFractPair K) = Int
 theorem coe_stream_nth_rat_eq :
     ((IntFractPair.stream q n).map (mapFr (↑)) : Option <| IntFractPair K) =
       IntFractPair.stream v n := by
-  induction' n with n IH
-  case zero =>
+  induction n with
+  | zero =>
     -- Porting note: was
     -- simp [IntFractPair.stream, coe_of_rat_eq v_eq_q]
     simp only [IntFractPair.stream, Option.map_some', coe_of_rat_eq v_eq_q]
-  case succ =>
+  | succ n IH =>
     rw [v_eq_q] at IH
-    cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
-    case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
-    case some =>
+    cases stream_q_nth_eq : IntFractPair.stream q n with
+    | none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
+    | some ifp_n =>
       cases' ifp_n with b fr
       cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
       · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
@@ -296,12 +296,12 @@ theorem stream_succ_nth_fr_num_lt_nth_fr_num_rat {ifp_n ifp_succ_n : IntFractPai
 theorem stream_nth_fr_num_le_fr_num_sub_n_rat :
     ∀ {ifp_n : IntFractPair ℚ},
       IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - n := by
-  induction' n with n IH
-  case zero =>
+  induction n with
+  | zero =>
     intro ifp_zero stream_zero_eq
     have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
     simp [le_refl, this.symm]
-  case succ =>
+  | succ n IH =>
     intro ifp_succ_n stream_succ_nth_eq
     suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
       rw [Int.ofNat_succ, sub_add_eq_sub_sub]

Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -120,9 +120,9 @@ theorem squashSeq_nth_of_not_terminated {gp_n gp_succ_n : Pair K} (s_nth_eq : s.
 
 /-- The values before the squashed position stay the same. -/
 theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m = s.get? m := by
-  cases s_succ_nth_eq : s.get? (n + 1)
-  case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
-  case some =>
+  cases s_succ_nth_eq : s.get? (n + 1) with
+  | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
+  | some =>
     obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n
     exact s.ge_stable n.le_succ s_succ_nth_eq
     obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m
@@ -134,11 +134,11 @@ theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m
 sequence at position `n`. -/
 theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n :
     (squashSeq s (n + 1)).tail = squashSeq s.tail n := by
-  cases' s_succ_succ_nth_eq : s.get? (n + 2) with gp_succ_succ_n
-  case none =>
+  cases s_succ_succ_nth_eq : s.get? (n + 2) with
+  | none =>
     cases s_succ_nth_eq : s.get? (n + 1) <;>
       simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
-  case some =>
+  | some gp_succ_succ_n =>
     obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n;
     exact s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
     -- apply extensionality with `m` and continue by cases `m = n`.
@@ -155,19 +155,19 @@ theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n :
 corresponding squashed sequence at the squashed position. -/
 theorem succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq :
     convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1) := by
-  cases' s_succ_nth_eq : s.get? <| n + 1 with gp_succ_n
-  case none =>
+  cases s_succ_nth_eq : s.get? <| n + 1 with
+  | none =>
     rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
       convergents'Aux_stable_step_of_terminated s_succ_nth_eq]
-  case some =>
-    induction' n with m IH generalizing s gp_succ_n
-    case zero =>
+  | some gp_succ_n =>
+    induction n generalizing s gp_succ_n with
+    | zero =>
       obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
       exact s.ge_stable zero_le_one s_succ_nth_eq
       have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
         squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
       simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
-    case succ =>
+    | succ m IH =>
       obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
       exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
       suffices
@@ -204,11 +204,11 @@ squashed gcf. -/
 /-- If the gcf already terminated at position `n`, nothing gets squashed. -/
 theorem squashGCF_eq_self_of_terminated (terminated_at_n : TerminatedAt g n) :
     squashGCF g n = g := by
-  cases n
-  case zero =>
+  cases n with
+  | zero =>
     change g.s.get? 0 = none at terminated_at_n
     simp only [convergents', squashGCF, convergents'Aux, terminated_at_n]
-  case succ =>
+  | succ =>
     cases g
     simp only [squashGCF, mk.injEq, true_and]
     exact squashSeq_eq_self_of_terminated terminated_at_n
@@ -224,11 +224,11 @@ theorem squashGCF_nth_of_lt {m : ℕ} (m_lt_n : m < n) :
 squashed position. -/
 theorem succ_nth_convergent'_eq_squashGCF_nth_convergent' :
     g.convergents' (n + 1) = (squashGCF g n).convergents' n := by
-  cases n
-  case zero =>
+  cases n with
+  | zero =>
     cases g_s_head_eq : g.s.get? 0 <;>
       simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
-  case succ =>
+  | succ =>
     simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents',
       squashGCF]
 #align generalized_continued_fraction.succ_nth_convergent'_eq_squash_gcf_nth_convergent' GeneralizedContinuedFraction.succ_nth_convergent'_eq_squashGCF_nth_convergent'
@@ -270,8 +270,8 @@ theorem succ_nth_convergent_eq_squashGCF_nth_convergent [Field K]
   · obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n
     exact Option.ne_none_iff_exists'.mp not_terminated_at_n
     have b_ne_zero : b ≠ 0 := nth_part_denom_ne_zero (part_denom_eq_s_b s_nth_eq)
-    cases' n with n'
-    case zero =>
+    cases n with
+    | zero =>
       suffices (b * g.h + a) / b = g.h + a / b by
         simpa [squashGCF, s_nth_eq, convergent_eq_conts_a_div_conts_b,
           continuants_recurrenceAux s_nth_eq zeroth_continuant_aux_eq_one_zero
@@ -280,7 +280,7 @@ theorem succ_nth_convergent_eq_squashGCF_nth_convergent [Field K]
         (b * g.h + a) / b = b * g.h / b + a / b := by ring
         -- requires `Field`, not `DivisionRing`
         _ = g.h + a / b := by rw [mul_div_cancel_left _ b_ne_zero]
-    case succ =>
+    | succ n' =>
       obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' :=
         g.s.ge_stable n'.le_succ s_nth_eq
       -- Notations
@@ -342,9 +342,9 @@ positivity criterion required here. The analogous result for them
 theorem convergents_eq_convergents' [LinearOrderedField K]
     (s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) :
     g.convergents n = g.convergents' n := by
-  induction' n with n IH generalizing g
-  case zero => simp
-  case succ =>
+  induction n generalizing g with
+  | zero => simp
+  | succ n IH =>
     let g' := squashGCF g n
     -- first replace the rhs with the squashed computation
     suffices g.convergents (n + 1) = g'.convergents' n by

Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean

@@ -45,12 +45,12 @@ theorem continuantsAux_stable_of_terminated (n_lt_m : n < m) (terminated_at_n :
 theorem convergents'Aux_stable_step_of_terminated {s : Stream'.Seq <| Pair K}
     (terminated_at_n : s.TerminatedAt n) : convergents'Aux s (n + 1) = convergents'Aux s n := by
   change s.get? n = none at terminated_at_n
-  induction' n with n IH generalizing s
-  case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
-  case succ =>
-    cases' s_head_eq : s.head with gp_head
-    case none => simp only [convergents'Aux, s_head_eq]
-    case some =>
+  induction n generalizing s with
+  | zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
+  | succ n IH =>
+    cases s_head_eq : s.head with
+    | none => simp only [convergents'Aux, s_head_eq]
+    | some gp_head =>
       have : s.tail.TerminatedAt n := by
         simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
       have := IH this

Mathlib/Algebra/FreeAlgebra.lean

@@ -371,21 +371,21 @@ def lift : (X → A) ≃ (FreeAlgebra R X →ₐ[R] A) :=
     right_inv := fun F ↦ by
       ext t
       rcases t with ⟨x⟩
-      induction x
-      case of =>
+      induction x with
+      | of =>
         change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
         simp only [Function.comp_apply, ι_def]
-      case ofScalar x =>
+      | ofScalar x =>
         change algebraMap _ _ x = F (algebraMap _ _ x)
         rw [AlgHom.commutes F _]
-      case add a b ha hb =>
+      | add a b ha hb =>
         -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
         -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
         let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
         let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
         change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
         rw [AlgHom.map_add, AlgHom.map_add, ha, hb]
-      case mul a b ha hb =>
+      | mul a b ha hb =>
         let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
         let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
         change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -213,10 +213,10 @@ theorem zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
 
 @[to_additive add_zsmul]
 theorem zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
-  induction' n using Int.induction_on with n ihn n ihn
-  case hz => simp
-  · simp only [← add_assoc, zpow_add_one, ihn, mul_assoc]
-  · rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, add_sub_assoc]
+  induction n using Int.induction_on with
+  | hz => simp
+  | hp n ihn => simp only [← add_assoc, zpow_add_one, ihn, mul_assoc]
+  | hn n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, add_sub_assoc]
 #align zpow_add zpow_add
 #align add_zsmul add_zsmul
 

Mathlib/Algebra/Lie/Free.lean

@@ -201,14 +201,14 @@ theorem liftAux_map_mul (f : X → L) (a b : lib R X) :
 
 theorem liftAux_spec (f : X → L) (a b : lib R X) (h : FreeLieAlgebra.Rel R X a b) :
     liftAux R f a = liftAux R f b := by
-  induction h
-  case lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]
-  case leibniz_lie a' b' c' =>
+  induction h with
+  | lie_self a' => simp only [liftAux_map_mul, NonUnitalAlgHom.map_zero, lie_self]
+  | leibniz_lie a' b' c' =>
     simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
-  case smul t a' b' _ h₂ => simp only [liftAux_map_smul, h₂]
-  case add_right a' b' c' _ h₂ => simp only [liftAux_map_add, h₂]
-  case mul_left a' b' c' _ h₂ => simp only [liftAux_map_mul, h₂]
-  case mul_right a' b' c' _ h₂ => simp only [liftAux_map_mul, h₂]
+  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
+  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
+  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
+  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
 #align free_lie_algebra.lift_aux_spec FreeLieAlgebra.liftAux_spec
 
 /-- The quotient map as a `NonUnitalAlgHom`. -/