Theorem: even_succ_odd (LeanCourse/Extra.lean)

State before:
n : ℕ
h : OddNat n
⊢ EvenNat (n + 1)
Tactic:
refine Odd.add_odd h ?_
State after:
n : ℕ
h : OddNat n
⊢ Odd 1

State before:
n : ℕ
h : OddNat n
⊢ Odd 1
Tactic:
norm_num
State after:
no goals