chore: avoid using cases' early (#6997)

This will help with my cleanup of the early library, facilitating moving tactics upstream.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Data/Sum/Basic.lean

@@ -583,21 +583,23 @@ theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y
 #align sum.lex.mono_right Sum.Lex.mono_right
 
 theorem lex_acc_inl {a} (aca : Acc r a) : Acc (Lex r s) (inl a) := by
-  induction' aca with a _ IH
-  constructor
-  intro y h
-  cases' h with a' _ h'
-  exact IH _ h'
+  induction aca with
+  | intro _ _ IH =>
+    constructor
+    intro y h
+    cases h with
+    | inl h' => exact IH _ h'
 #align sum.lex_acc_inl Sum.lex_acc_inl
 
 theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
     Acc (Lex r s) (inr b) := by
-  induction' acb with b _ IH
-  constructor
-  intro y h
-  cases' h with _ _ _ b' _ h' a
-  · exact IH _ h'
-  · exact aca _
+  induction acb with
+  | intro _ _ IH =>
+    constructor
+    intro y h
+    cases h with
+    | inr h' => exact IH _ h'
+    | sep => exact aca _
 #align sum.lex_acc_inr Sum.lex_acc_inr
 
 theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=

Mathlib/Logic/Function/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Logic.Nonempty
-import Mathlib.Tactic.Cases
 import Mathlib.Init.Set
 
 #align_import logic.function.basic from "leanprover-community/mathlib"@"29cb56a7b35f72758b05a30490e1f10bd62c35c1"
@@ -293,7 +292,7 @@ theorem cantor_injective {α : Type*} (f : Set α → α) : ¬Injective f
 theorem not_surjective_Type {α : Type u} (f : α → Type max u v) : ¬Surjective f := by
   intro hf
   let T : Type max u v := Sigma f
-  cases' hf (Set T) with U hU
+  cases hf (Set T) with | intro U hU =>
   let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
   have hg : Injective g := by
     intro s t h

Mathlib/Logic/Function/Iterate.lean

@@ -119,10 +119,12 @@ theorem iterate_right {f : α → β} {ga : α → α} {gb : β → β} (h : Sem
 
 theorem iterate_left {g : ℕ → α → α} (H : ∀ n, Semiconj f (g n) (g <| n + 1)) (n k : ℕ) :
     Semiconj f^[n] (g k) (g <| n + k) := by
-  induction' n with n ihn generalizing k
-  · rw [Nat.zero_add]
+  induction n generalizing k with
+  | zero =>
+    rw [Nat.zero_add]
     exact id_left
-  · rw [Nat.succ_eq_add_one, Nat.add_right_comm, Nat.add_assoc]
+  | succ n ihn =>
+    rw [Nat.succ_eq_add_one, Nat.add_right_comm, Nat.add_assoc]
     exact (H k).comp_left (ihn (k + 1))
 #align function.semiconj.iterate_left Function.Semiconj.iterate_left
 
@@ -151,10 +153,11 @@ theorem iterate_eq_of_map_eq (h : Commute f g) (n : ℕ) {x} (hx : f x = g x) :
 #align function.commute.iterate_eq_of_map_eq Function.Commute.iterate_eq_of_map_eq
 
 theorem comp_iterate (h : Commute f g) (n : ℕ) : (f ∘ g)^[n] = f^[n] ∘ g^[n] := by
-  induction' n with n ihn
-  · rfl
-  funext x
-  simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
+  induction n with
+  | zero => rfl
+  | succ n ihn =>
+    funext x
+    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
 #align function.commute.comp_iterate Function.Commute.comp_iterate
 
 variable (f)
@@ -257,9 +260,9 @@ open Function
 
 theorem foldl_const (f : α → α) (a : α) (l : List β) :
     l.foldl (fun b _ ↦ f b) a = f^[l.length] a := by
-  induction' l with b l H generalizing a
-  · rfl
-  · rw [length_cons, foldl, iterate_succ_apply, H]
+  induction l generalizing a with
+  | nil => rfl
+  | cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]
 #align list.foldl_const List.foldl_const
 
 theorem foldr_const (f : β → β) (b : β) : ∀ l : List α, l.foldr (fun _ ↦ f) b = f^[l.length] b