Theorem: three_plus_two_five (Fpil/Chap10/Sec03.lean)

State before:
n : Nat
⊢ IsThree n → IsFive (n + 2)
Tactic:
intro three
State after:
n : Nat
three : IsThree n
⊢ IsFive (n + 2)

State before:
n : Nat
three : IsThree n
⊢ IsFive (n + 2)
Tactic:
cases three with
| isThree => constructor
State after:
no goals

State before:
case isThree

⊢ IsFive (3 + 2)
Tactic:
constructor
State after:
no goals