Theorem: LeanDemo.succ_add (LeanMeetup/Demo01.lean)

State before:
x y : Nat
⊢ succ x + y = succ (x + y)
Tactic:
induction y
State after:
case zero
x : Nat
⊢ succ x + zero = succ (x + zero)

case succ
x n✝ : Nat
n_ih✝ : succ x + n✝ = succ (x + n✝)
⊢ succ x + succ n✝ = succ (x + succ n✝)

State before:
x : Nat
⊢ succ x + zero = succ (x + zero)
Tactic:
case zero =>      rfl
State after:
no goals

State before:
x y : Nat
ih : succ x + y = succ (x + y)
⊢ succ x + succ y = succ (x + succ y)
Tactic:
case succ y ih => rw [add_succ, add_succ, ih]
State after:
no goals

State before:
x : Nat
⊢ succ x + zero = succ (x + zero)
Tactic:
rfl
State after:
no goals

State before:
x y : Nat
ih : succ x + y = succ (x + y)
⊢ succ x + succ y = succ (x + succ y)
Tactic:
rw [add_succ, add_succ, ih]
State after:
no goals