From f8adb449fee242aada7b4e2991d2e00d83f2866f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Mar 2021 19:48:25 -0700 Subject: [PATCH] fix: doc --- doc/tactics.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/tactics.md b/doc/tactics.md index 1433277483..6c7dfca37c 100644 --- a/doc/tactics.md +++ b/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