Theorem: add_one_odd_of_even (LeanTeaching/TD/TD03.lean)

State before:
n : ℕ
h : Even n
⊢ Odd (n + 1)
Tactic:
apply Even.add_odd
State after:
case a
n : ℕ
h : Even n
⊢ Even n

case a
n : ℕ
h : Even n
⊢ Odd 1

State before:
case a
n : ℕ
h : Even n
⊢ Even n
Tactic:
exact h
State after:
no goals

State before:
case a
n : ℕ
h : Even n
⊢ Odd 1
Tactic:
exact odd_one
State after:
no goals