fix: doc

doc/tactics.md

@@ -171,7 +171,7 @@ theorem Nat.mod.inductionOn
 -/
 
 theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
-  induction x, y using Nat.mod.inductionOn generalizing h with
+  induction x, y using Nat.mod.inductionOn with
   | ind x y h₁ ih =>
     rw [Nat.mod_eq_sub_mod h₁.2]
     exact ih h
@@ -239,7 +239,7 @@ Here is a similar proof that uses the `induction` tactic instead of recursion.
 #  | tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
 # infix:50 "∈" => Mem
 theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
-  induction as generalizing h with
+  induction as with
   | nil          => cases h
   | cons b bs ih => cases h with
     | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
@@ -263,7 +263,7 @@ macro "obtain " p:term " from " d:term : tactic =>
   `(tactic| match $d:term with | $p:term => ?_)
 
 theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
-  induction as generalizing h with
+  induction as with
   | cons b bs ih => cases h with
     | tail a b bs h =>
       obtain ⟨s, ⟨t, h⟩⟩ from ih h