Refactor uses to rename_i that have easy fixes (#2429)

Mathlib/Combinatorics/Young/SemistandardTableau.lean

@@ -127,16 +127,16 @@ theorem zeros {μ : YoungDiagram} (T : Ssyt μ) {i j : ℕ} (not_cell : (i, j) 
 
 theorem row_weak_of_le {μ : YoungDiagram} (T : Ssyt μ) {i j1 j2 : ℕ} (hj : j1 ≤ j2)
     (cell : (i, j2) ∈ μ) : T i j1 ≤ T i j2 := by
-  cases eq_or_lt_of_le hj <;> rename_i h
-  rw [h]
-  exact T.row_weak h cell
+  cases' eq_or_lt_of_le hj with h h
+  . rw [h]
+  . exact T.row_weak h cell
 #align ssyt.row_weak_of_le Ssyt.row_weak_of_le
 
 theorem col_weak {μ : YoungDiagram} (T : Ssyt μ) {i1 i2 j : ℕ} (hi : i1 ≤ i2) (cell : (i2, j) ∈ μ) :
     T i1 j ≤ T i2 j := by
-  cases eq_or_lt_of_le hi <;> rename_i h
-  rw [h]
-  exact le_of_lt (T.col_strict h cell)
+  cases' eq_or_lt_of_le hi with h h
+  . rw [h]
+  . exact le_of_lt (T.col_strict h cell)
 #align ssyt.col_weak Ssyt.col_weak
 
 /-- The "highest weight" SSYT of a given shape has all i's in row i, for each i. -/

Mathlib/Data/Finmap.lean

@@ -528,12 +528,11 @@ theorem toFinmap_cons (a : α) (b : β a) (xs : List (Sigma β)) :
 
 theorem mem_list_toFinmap (a : α) (xs : List (Sigma β)) :
     a ∈ xs.toFinmap ↔ ∃ b : β a, Sigma.mk a b ∈ xs := by
-  induction' xs with x xs <;> [skip, cases x] <;>
+  induction' xs with x xs <;> [skip, cases' x with fst_i snd_i] <;>
       -- Porting note: `Sigma.mk.inj_iff` required because `simp` behaves differently
       simp only [toFinmap_cons, *, not_mem_empty, exists_or, not_mem_nil, toFinmap_nil,
         exists_false, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff];
       apply or_congr _ Iff.rfl
-  rename_i tail_ih fst_i snd_i
   conv =>
     lhs
     rw [← and_true_iff (a = fst_i)]

Mathlib/Data/Finsupp/Pointwise.lean

@@ -60,7 +60,7 @@ theorem support_mul [DecidableEq α] {g₁ g₂ : α →₀ β} :
   rw [← not_or]
   intro w
   apply h
-  cases w <;> (rename_i w ; rw [w] ; simp)
+  cases' w with w w <;> (rw [w] ; simp)
 #align finsupp.support_mul Finsupp.support_mul
 
 instance : MulZeroClass (α →₀ β) :=

Mathlib/Data/LazyList/Basic.lean

@@ -55,10 +55,10 @@ def listEquivLazyList (α : Type _) : List α ≃ LazyList α
   invFun := LazyList.toList
   right_inv := by
     intro xs
-    induction xs using LazyList.rec
+    induction' xs using LazyList.rec with _ _ _ _ ih
     rfl
     simpa only [toList, ofList, cons.injEq, true_and]
-    rename_i ih; rw [Thunk.get, ih]
+    rw [Thunk.get, ih]
   left_inv := by
     intro xs
     induction xs
@@ -93,25 +93,24 @@ instance : Traversable LazyList
 
 instance : IsLawfulTraversable LazyList := by
   apply Equiv.isLawfulTraversable' listEquivLazyList <;> intros <;> ext <;> rename_i f xs
-  · induction xs using LazyList.rec
+  · induction' xs using LazyList.rec with _ _ _ _ ih
     rfl
     simpa only [Equiv.map, Functor.map, listEquivLazyList, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk,
       LazyList.traverse, Seq.seq, toList, ofList, cons.injEq, true_and]
-    rename_i ih; ext; apply ih
+    ext; apply ih
   · simp only [Equiv.map, listEquivLazyList, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, comp,
       Functor.mapConst]
-    induction xs using LazyList.rec
+    induction' xs using LazyList.rec with _ _ _ _ ih
     rfl
     simpa only [toList, ofList, LazyList.traverse, Seq.seq, Functor.map, cons.injEq, true_and]
-    rename_i ih; congr; apply ih
+    congr; apply ih
   · simp only [traverse, Equiv.traverse, listEquivLazyList, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk]
-    induction xs using LazyList.rec
+    induction' xs using LazyList.rec with _ tl ih _ ih
     simp only [List.traverse, map_pure]; rfl
-    rename_i tl ih
     have : tl.get.traverse f = ofList <$> tl.get.toList.traverse f := ih
     simp only [traverse._eq_2, ih, Functor.map_map, seq_map_assoc, toList, List.traverse, map_seq]
-    rfl
-    rename_i ih; apply ih
+    . rfl
+    . apply ih
 
 /-- `init xs`, if `xs` non-empty, drops the last element of the list.
 Otherwise, return the empty list. -/
@@ -167,16 +166,18 @@ instance : Monad LazyList where
 
 -- Porting note: Added `Thunk.pure` to definition.
 theorem append_nil {α} (xs : LazyList α) : xs.append (Thunk.pure LazyList.nil) = xs := by
-  induction xs using LazyList.rec; rfl
-  simpa only [append, cons.injEq, true_and]
-  ext; rename_i ih; apply ih
+  induction' xs using LazyList.rec with _ _ _ _ ih
+  . rfl
+  . simpa only [append, cons.injEq, true_and]
+  . ext; apply ih
 #align lazy_list.append_nil LazyList.append_nil
 
 theorem append_assoc {α} (xs ys zs : LazyList α) :
     (xs.append ys).append zs = xs.append (ys.append zs) := by
-  induction xs using LazyList.rec; rfl
-  simpa only [append, cons.injEq, true_and]
-  ext; rename_i ih; apply ih
+  induction' xs using LazyList.rec with _ _ _ _ ih
+  . rfl
+  . simpa only [append, cons.injEq, true_and]
+  . ext; apply ih
 #align lazy_list.append_assoc LazyList.append_assoc
 
 -- Porting note: Rewrote proof of `append_bind`.
@@ -195,23 +196,26 @@ instance : LawfulMonad LazyList := LawfulMonad.mk'
   (bind_pure_comp := by
     intro _ _ f xs
     simp only [bind, Functor.map, pure, singleton]
-    induction xs using LazyList.rec; rfl
-    simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]; congr
-    rename_i ih; ext; apply ih)
+    induction' xs using LazyList.rec with _ _ _ _ ih
+    . rfl
+    . simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]; congr
+    . ext; apply ih)
   (pure_bind := by
     intros
     simp only [bind, pure, singleton, LazyList.bind]
     apply append_nil)
   (bind_assoc := by
-    intros; rename_i xs _ _
-    induction xs using LazyList.rec; rfl
-    simp only [bind, LazyList.bind, append_bind]; congr
-    rename_i ih; congr; funext; apply ih)
+    intro _ _ _ xs _ _
+    induction' xs using LazyList.rec with _ _ _ _ ih
+    . rfl
+    . simp only [bind, LazyList.bind, append_bind]; congr
+    . congr; funext; apply ih)
   (id_map := by
     intro _ xs
-    induction xs using LazyList.rec; rfl
-    simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]
-    rename_i ih; ext; apply ih)
+    induction' xs using LazyList.rec with _ _ _ _ ih
+    . rfl
+    . simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]
+    . ext; apply ih)
 
 -- Porting note: This is a dubious translation. In the warning, u1 and u3 are swapped.
 /-- Try applying function `f` to every element of a `LazyList` and

Mathlib/Data/Nat/Fib.lean

@@ -260,11 +260,9 @@ theorem fast_fib_eq (n : ℕ) : fastFib n = fib n := by rw [fastFib, fast_fib_au
 #align nat.fast_fib_eq Nat.fast_fib_eq
 
 theorem gcd_fib_add_self (m n : ℕ) : gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n) := by
-  cases Nat.eq_zero_or_pos n
-  · rename_i h
-    rw [h]
+  cases' Nat.eq_zero_or_pos n with h h
+  · rw [h]
     simp
-  rename_i h
   replace h := Nat.succ_pred_eq_of_pos h; rw [← h, succ_eq_add_one]
   calc
     gcd (fib m) (fib (n.pred + 1 + m)) =
@@ -293,7 +291,7 @@ theorem gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m))
 /-- `fib n` is a strong divisibility sequence,
   see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers -/
 theorem fib_gcd (m n : ℕ) : fib (gcd m n) = gcd (fib m) (fib n) := by
-  cases le_total m n <;> rename_i h
+  cases' le_total m n with h h
   case inl =>
       apply @Nat.gcd.induction _ m n
       case H0 => simp

Mathlib/Data/PFunctor/Univariate/M.lean

@@ -400,8 +400,8 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem agree'_refl {n : ℕ} (x : M F) : Agree' n x x := by
-  induction n generalizing x <;> induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl
-  rename_i n_ih _ _
+  induction' n with _ n_ih generalizing x <;>
+  induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl
   intros
   apply n_ih
 set_option linter.uppercaseLean3 false in
@@ -422,8 +422,7 @@ theorem agree_iff_agree' {n : ℕ} (x y : M F) :
       apply hagree
   · induction' n with _ n_ih generalizing x y
     constructor
-    · cases h
-      rename_i a x' y' _ _ _
+    · cases' h with _ _ _ a x' y'
       induction' x using PFunctor.M.casesOn' with x_a x_f
       induction' y using PFunctor.M.casesOn' with y_a y_f
       simp only [approx_mk]

Mathlib/Data/Set/Intervals/Basic.lean

@@ -1361,10 +1361,9 @@ theorem Icc_union_Ici' (h₁ : c ≤ b) : Icc a b ∪ Ici c = Ici (min a c) := b
 theorem Icc_union_Ici (h : c ≤ max a b) : Icc a b ∪ Ici c = Ici (min a c) := by
   cases' le_or_lt a b with hab hab <;> simp [hab] at h
   · exact Icc_union_Ici' h
-  · cases h
+  · cases' h with h h
     · simp [*]
-    · rename_i h
-      have hca : c ≤ a := h.trans hab.le
+    · have hca : c ≤ a := h.trans hab.le
       simp [*]
 #align set.Icc_union_Ici Set.Icc_union_Ici
 
@@ -1480,9 +1479,8 @@ theorem Iic_union_Icc' (h₁ : c ≤ b) : Iic b ∪ Icc c d = Iic (max b d) := b
 theorem Iic_union_Icc (h : min c d ≤ b) : Iic b ∪ Icc c d = Iic (max b d) := by
   cases' le_or_lt c d with hcd hcd <;> simp [hcd] at h
   · exact Iic_union_Icc' h
-  · cases h
-    · rename_i h
-      have hdb : d ≤ b := hcd.le.trans h
+  · cases' h with h h
+    · have hdb : d ≤ b := hcd.le.trans h
       simp [*]
     · simp [*]
 #align set.Iic_union_Icc Set.Iic_union_Icc

Mathlib/Data/Set/Intervals/Monotone.lean

@@ -236,9 +236,8 @@ theorem strictMonoOn_Iic_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] {n : 
   obtain ⟨i, rfl⟩ := hxy.le.exists_succ_iterate
   induction' i with k ih
   · simp at hxy
-  cases k
+  cases' k with k
   · exact hψ _ (lt_of_lt_of_le hxy hy)
-  rename_i k
   rw [Set.mem_Iic] at *
   simp only [Function.iterate_succ', Function.comp_apply] at ih hxy hy⊢
   by_cases hmax : IsMax ((succ^[k]) x)

Mathlib/Data/Sum/Interval.lean

@@ -50,7 +50,7 @@ theorem mem_sumLift₂ :
       (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
         ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂ := by
   constructor
-  · cases a <;> cases b <;> rename_i a b
+  · cases' a with a a <;> cases' b with b b
     · rw [sumLift₂, mem_map]
       rintro ⟨c, hc, rfl⟩
       exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩

Mathlib/Data/Sym/Sym2.lean

@@ -755,8 +755,7 @@ theorem filter_image_quotient_mk''_isDiag [DecidableEq α] (s : Finset α) :
     ((s ×ᶠ s).image Quotient.mk'').filter IsDiag = s.diag.image Quotient.mk'' :=
   by
   ext z
-  induction z using Sym2.inductionOn
-  rename_i x y
+  induction' z using Sym2.inductionOn
   simp only [mem_image, mem_diag, exists_prop, mem_filter, Prod.exists, mem_product]
   constructor
   · rintro ⟨⟨a, b, ⟨ha, hb⟩, (h : Quotient.mk _ _ = _)⟩, hab⟩

Mathlib/Data/TypeVec.lean

@@ -551,19 +551,17 @@ end
 theorem prod_fst_mk {α β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) :
   TypeVec.prod.fst i (prod.mk i a b) = a :=
 by
-  induction i
+  induction' i with _ _ _ i_ih
   simp_all only [prod.fst, prod.mk]
-  rename_i i_ih
   apply i_ih
 #align typevec.prod_fst_mk TypeVec.prod_fst_mk
 
 @[simp]
 theorem prod_snd_mk {α β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) :
   TypeVec.prod.snd i (prod.mk i a b) = b :=
 by
-  induction i
+  induction' i with _ _ _ i_ih
   simp_all [prod.snd, prod.mk]
-  rename_i i_ih
   apply i_ih
 #align typevec.prod_snd_mk TypeVec.prod_snd_mk
 
@@ -611,9 +609,8 @@ theorem snd_diag {α : TypeVec n} : TypeVec.prod.snd ⊚ (prod.diag : α ⟹ _)
 theorem repeatEq_iff_eq {α : TypeVec n} {i x y} :
   ofRepeat (repeatEq α i (prod.mk _ x y)) ↔ x = y :=
 by
-  induction i
+  induction' i with _ _ _ i_ih
   rfl
-  rename_i i i_ih
   erw [repeatEq, i_ih]
 #align typevec.repeat_eq_iff_eq TypeVec.repeatEq_iff_eq
 
@@ -676,20 +673,18 @@ theorem subtypeVal_nil {α : TypeVec.{u} 0} (ps : α ⟹ «repeat» 0 Prop) :
 theorem diag_sub_val {n} {α : TypeVec.{u} n} : subtypeVal (repeatEq α) ⊚ diagSub = prod.diag :=
 by
   ext i x
-  induction i
+  induction' i with _ _ _ i_ih
   simp [prod.diag, diagSub, repeatEq, subtypeVal, comp]
-  rename_i _ i_ih
   apply @i_ih (drop α)
 #align typevec.diag_sub_val TypeVec.diag_sub_val
 
 theorem prod_id : ∀ {n} {α β : TypeVec.{u} n}, (id ⊗' id) = (id : α ⊗ β ⟹ _) := by
   intros
   ext (i a)
-  induction i
+  induction' i with _ _ _ i_ih
   · cases a
     rfl
-  · rename_i i_ih _ _
-    apply i_ih
+  · apply i_ih
 
 #align typevec.prod_id TypeVec.prod_id
 
@@ -811,10 +806,9 @@ theorem prod_map_id {α β : TypeVec n} : (@TypeVec.id _ α ⊗' @TypeVec.id _ 
 @[simp]
 theorem subtypeVal_diagSub {α : TypeVec n} : subtypeVal (repeatEq α) ⊚ diagSub = prod.diag := by
   ext i x
-  induction i
+  induction' i with _ _ _ i_ih
   . simp [comp, diagSub, subtypeVal, prod.diag]
-  . rename_i i i_ih
-    simp [prod.diag]
+  . simp [prod.diag]
     simp [comp, diagSub, subtypeVal, prod.diag] at *
     apply @i_ih (drop _)
 #align typevec.subtype_val_diag_sub TypeVec.subtypeVal_diagSub

Mathlib/Init/Data/Nat/Bitwise.lean

@@ -92,17 +92,11 @@ theorem mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
   have := congr_arg bodd (mod_add_div n 2)
   simp [not] at this
   have _ : ∀ b, and false b = false := by
-    intros
-    rename_i b
-    cases b
-    case false => rfl
-    case true => rfl
+    intro b
+    cases b <;> rfl
   have _ : ∀ b, bxor b false = b := by
-    intros
-    rename_i b'
-    cases b'
-    case false => rfl
-    case true => rfl
+    intro b
+    cases b <;> rfl
   rw [← this]
   cases' mod_two_eq_zero_or_one n with h h <;> rw [h] <;> rfl
 #align nat.mod_two_of_bodd Nat.mod_two_of_bodd
@@ -123,8 +117,7 @@ theorem div2_two : div2 2 = 1 :=
 @[simp]
 theorem div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
   simp only [bodd, boddDiv2, div2]
-  cases boddDiv2 n
-  rename_i fst snd
+  cases' boddDiv2 n with fst snd
   cases fst
   case mk.false =>
     simp
@@ -222,8 +215,7 @@ def shiftr : ℕ → ℕ → ℕ
 #align nat.shiftr Nat.shiftr
 
 theorem shiftr_zero : ∀ n, shiftr 0 n = 0 := by
-  intros
-  rename_i n
+  intro n
   induction' n with n IH
   case zero =>
     rw [shiftr]

Mathlib/Logic/Encodable/Basic.lean

@@ -567,10 +567,9 @@ private def good : Option α → Prop
   | some a => p a
   | none => False
 
--- TODO: remove `rename_i`
-private def decidable_good : DecidablePred (good p)
-  | n => by cases' n with a a <;>
-         unfold good <;> rename_i x <;> cases x <;> dsimp <;> infer_instance
+private def decidable_good : DecidablePred (good p) :=
+  fun n => by
+    cases n <;> unfold good <;> dsimp <;> infer_instance
 attribute [local instance] decidable_good
 
 open Encodable