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

State before:
⊢ ∀ (n' : Nat), Even n' → ∀ (n : Nat), n' ≠ Nat.succ (n + n)
Tactic:
intro n' hn'
State after:
n' : Nat
hn' : Even n'
⊢ ∀ (n : Nat), n' ≠ Nat.succ (n + n)

State before:
n' : Nat
hn' : Even n'
⊢ ∀ (n : Nat), n' ≠ Nat.succ (n + n)
Tactic:
induction hn' with
| zero => simp_all
| succSucc x hx ih =>
  intro n hn
  cases x <;> cases n <;> simp_all <;> simp_arith at *
  case succSucc.succ.succ y m =>
    apply ih m
    assumption
State after:
no goals

State before:
case zero
n' : Nat
⊢ ∀ (n : Nat), 0 ≠ Nat.succ (n + n)
Tactic:
simp_all
State after:
no goals

State before:
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
⊢ ∀ (n : Nat), Nat.succ (Nat.succ x) ≠ Nat.succ (n + n)
Tactic:
intro n hn
State after:
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
n : Nat
hn : Nat.succ (Nat.succ x) = Nat.succ (n + n)
⊢ False

State before:
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
n : Nat
hn : Nat.succ (Nat.succ x) = Nat.succ (n + n)
⊢ False
Tactic:
cases x <;> cases n <;> simp_all <;> simp_arith at *
State after:
case succSucc.succ.succ
n' n✝¹ : Nat
hx : Even (Nat.succ n✝¹)
n✝ : Nat
ih : ∀ (n : Nat), ¬n✝¹ = 2 * n
hn : n✝¹ = 2 * n✝
⊢ False

State before:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ False
Tactic:
case succSucc.succ.succ y m =>
  apply ih m
  assumption
State after:
no goals

State before:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ False
Tactic:
apply ih m
State after:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ y = 2 * m

State before:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ y = 2 * m
Tactic:
assumption
State after:
no goals