Theorem: bar2 (BrownCs22.lean)

State before:
n : ℕ
⊢ odd (a (n + 1))
Tactic:
induction' n with n h1 h2
State after:
case zero

⊢ odd (a (Nat.zero + 1))

case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))

State before:
case zero

⊢ odd (a (Nat.zero + 1))

case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))
Tactic:
. use 2
  rfl
State after:
case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))

State before:
case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))
Tactic:
cases' h1 with k hk
State after:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ odd (a (Nat.succ n + 1))

State before:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ odd (a (Nat.succ n + 1))
Tactic:
use 5*k - 3*a n + 2
State after:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ a (Nat.succ n + 1) = 2 * (5 * k - 3 * a n + 2) + 1

State before:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ a (Nat.succ n + 1) = 2 * (5 * k - 3 * a n + 2) + 1
Tactic:
rw [helper]
State after:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ 5 * a (n + 1) - 6 * a n = 2 * (5 * k - 3 * a n + 2) + 1

State before:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ 5 * a (n + 1) - 6 * a n = 2 * (5 * k - 3 * a n + 2) + 1
Tactic:
linarith
State after:
no goals