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

State before:
n m : Nat
⊢ Even n → Even m → Even (n + m)
Tactic:
intro h1
State after:
n m : Nat
h1 : Even n
⊢ Even m → Even (n + m)

State before:
n m : Nat
h1 : Even n
⊢ Even m → Even (n + m)
Tactic:
induction h1 with
| zero =>
  intro h
  simp_arith
  assumption
| succSucc x xh ih =>
  intro h
  simp_arith
  constructor
  simp_arith
  apply ih
  assumption
State after:
no goals

State before:
case zero
n m : Nat
⊢ Even m → Even (0 + m)
Tactic:
intro h
State after:
case zero
n m : Nat
h : Even m
⊢ Even (0 + m)

State before:
case zero
n m : Nat
h : Even m
⊢ Even (0 + m)
Tactic:
simp_arith
State after:
case zero
n m : Nat
h : Even m
⊢ Even m

State before:
case zero
n m : Nat
h : Even m
⊢ Even m
Tactic:
assumption
State after:
no goals

State before:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
⊢ Even m → Even (Nat.succ (Nat.succ x) + m)
Tactic:
intro h
State after:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (Nat.succ (Nat.succ x) + m)

State before:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (Nat.succ (Nat.succ x) + m)
Tactic:
simp_arith
State after:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (x + m + 2)

State before:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (x + m + 2)
Tactic:
constructor
State after:
case succSucc.a
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (x + m)