Theorem: foo (BrownCs22.lean)

State before:
n : ℕ
⊢ a n = 2 ^ n + 3 ^ n
Tactic:
induction' n using Nat.two_step_induction with n h1 h2
State after:
case H1

⊢ a 0 = 2 ^ 0 + 3 ^ 0

case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)

State before:
case H1

⊢ a 0 = 2 ^ 0 + 3 ^ 0

case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Tactic:
. rfl
State after:
case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)

State before:
case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Tactic:
. rfl
State after:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)

State before:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Tactic:
simp [Nat.succ_eq_add_one] at *
State after:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 1 + 1) = 2 ^ (n + 1 + 1) + 3 ^ (n + 1 + 1)

State before:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 1 + 1) = 2 ^ (n + 1 + 1) + 3 ^ (n + 1 + 1)
Tactic:
calc
  a (n + 2) 
    = (5 : ℤ) * (2 ^ (n + 1) + 3 ^ (n + 1)) - 
        6 * (2 ^ n + 3 ^ n) := by linarith [helper n]
  _ = (2 : ℤ) ^ (n + 2) + 3 ^ (n + 2) := by ring
State after:
no goals

State before:
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 2) = 5 * (2 ^ (n + 1) + 3 ^ (n + 1)) - 6 * (2 ^ n + 3 ^ n)
Tactic:
linarith [helper n]
State after:
no goals

State before:
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ 5 * (2 ^ (n + 1) + 3 ^ (n + 1)) - 6 * (2 ^ n + 3 ^ n) = 2 ^ (n + 2) + 3 ^ (n + 2)
Tactic:
ring
State after:
no goals