Theorem: bar (BrownCs22.lean)

State before:
n : ℕ
⊢ n ≥ 1 → odd (_root_.a n)
Tactic:
induction' n using Nat.two_step_induction with n h1 h2
State after:
case H1

⊢ 0 ≥ 1 → odd (_root_.a 0)

case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))

State before:
case H1

⊢ 0 ≥ 1 → odd (_root_.a 0)

case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Tactic:
. norm_num
State after:
case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))

State before:
case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Tactic:
. intro h
  use 2
  rfl
State after:
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))

State before:
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Tactic:
simp only [Nat.succ_eq_add_one] at *
State after:
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : n + 1 ≥ 1 → odd (_root_.a (n + 1))
⊢ n + 1 + 1 ≥ 1 → odd (_root_.a (n + 1 + 1))