Theorem: LoVe.odd_5 (LoVe/Labs/Lab5Solution.lean)

State before:
⊢ Odd 5
Tactic:
intro ho5
State after:
ho5 : Even 5
⊢ False

State before:
ho5 : Even 5
⊢ False
Tactic:
cases ho5 with
| add_two _ ho3 =>
  cases ho3 with
  | add_two _ ho1 =>
    cases ho1
State after:
no goals

State before:
case add_two
ho3 : Even 3
⊢ False
Tactic:
cases ho3 with
| add_two _ ho1 =>
  cases ho1
State after:
no goals

State before:
case add_two.add_two
ho1 : Even 1
⊢ False
Tactic:
cases ho1
State after:
no goals