chore: review uses of generalize (#7126)

This PR looks at some uses of the `generalize` tactic, especially when
used in conjunction with `induction`.

src/Init/Data/BitVec/Bitblast.lean

@@ -1034,11 +1034,10 @@ theorem divRec_succ (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
 theorem lawful_divRec {args : DivModArgs w} {qr : DivModState w}
     (h : DivModState.Lawful args qr) :
     DivModState.Lawful args (divRec qr.wn args qr) := by
-  generalize hm : qr.wn = m
-  induction m generalizing qr
-  case zero =>
+  induction hm : qr.wn generalizing qr with
+  | zero =>
     exact h
-  case succ wn' ih =>
+  | succ wn' ih =>
     simp only [divRec_succ]
     apply ih
     · apply lawful_divSubtractShift
@@ -1052,11 +1051,10 @@ theorem lawful_divRec {args : DivModArgs w} {qr : DivModState w}
 @[simp]
 theorem wn_divRec (args : DivModArgs w) (qr : DivModState w) :
     (divRec qr.wn args qr).wn = 0 := by
-  generalize hm : qr.wn = m
-  induction m generalizing qr
-  case zero =>
+  induction hm : qr.wn generalizing qr with
+  | zero =>
     assumption
-  case succ wn' ih =>
+  | succ wn' ih =>
     apply ih
     simp only [divSubtractShift, hm]
     split <;> rfl

src/Init/Data/List/Monadic.lean

@@ -321,24 +321,21 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
     forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
       l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
   simp only [forIn'_eq_foldlM]
-  generalize l.attach = l'
-  induction l' generalizing init <;> simp_all
+  induction l.attach generalizing init <;> simp_all
 
 theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
     (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) :
     forIn' l init (fun a m b => pure (.yield (f a m b))) =
       pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
   simp only [forIn'_eq_foldlM]
-  generalize l.attach = l'
-  induction l' generalizing init <;> simp_all
+  induction l.attach generalizing init <;> simp_all
 
 @[simp] theorem forIn'_yield_eq_foldl
     (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) :
     forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
       l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
   simp only [forIn'_eq_foldlM]
-  generalize l.attach = l'
-  induction l' generalizing init <;> simp_all
+  induction l.attach generalizing init <;> simp_all
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     (l : List α) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :

src/Init/Data/List/Sublist.lean

@@ -150,8 +150,8 @@ theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l
   | slnil => exact h₁
   | cons _ _ IH => exact (IH h₁).cons _
   | @cons₂ l₂ _ a _ IH =>
-    generalize e : a :: l₂ = l₂'
-    match e ▸ h₁ with
+    generalize e : a :: l₂ = l₂' at h₁
+    match h₁ with
     | .slnil => apply nil_sublist
     | .cons a' h₁' => cases e; apply (IH h₁').cons
     | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂

src/Std/Data/DHashMap/Internal/WF.lean

@@ -69,8 +69,7 @@ theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a 
     l.fold (fun acc k v => f k v :: acc) acc =
       ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc := by
   rw [fold_eq, ← Array.foldl_toList, toListModel]
-  generalize l.buckets.toList = l
-  induction l generalizing acc with
+  induction l.buckets.toList generalizing acc with
   | nil => simp
   | cons x xs ih =>
       rw [foldl_cons, ih, AssocList.foldl_apply]
@@ -93,8 +92,7 @@ theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β
     l.foldRev (fun acc k v => f k v :: acc) acc =
       ((toListModel l.buckets).map (fun p => f p.1 p.2)) ++ acc := by
   rw [foldRev_eq, ← Array.foldr_toList, toListModel]
-  generalize l.buckets.toList = l
-  induction l generalizing acc with
+  induction l.buckets.toList generalizing acc with
   | nil => simp
   | cons x xs ih =>
       rw [foldr_cons, ih, AssocList.foldr_apply]