Theorem: Cpdt.Chapter4.even_contra (Cpdt/Chapter4/RecPred.lean)

State before:
n : Nat
⊢ Even (Nat.succ (n + n)) → False
Tactic:
intro h
State after:
n : Nat
h : Even (Nat.succ (n + n))
⊢ False

State before:
n : Nat
h : Even (Nat.succ (n + n))
⊢ False
Tactic:
apply even_contra_helper
State after:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Even ?n'

case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ ?n' = Nat.succ (?n + ?n)

case n'
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

State before:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Even ?n'

case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ ?n' = Nat.succ (?n + ?n)

case n'
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat
Tactic:
assumption
State after:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat.succ (n + n) = Nat.succ (?n + ?n)

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

State before:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat.succ (n + n) = Nat.succ (?n + ?n)

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat
Tactic:
rfl
State after:
no goals