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

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

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

State before:
x : Nat
⊢ x + zero = zero + x
Tactic:
case zero =>
  rw [←zero_eq, zero_add, add_zero]
State after:
no goals

State before:
x y : Nat
ih : x + y = y + x
⊢ x + succ y = succ y + x
Tactic:
case succ y ih =>
  sorry
State after:
no goals

State before:
x : Nat
⊢ x + zero = zero + x
Tactic:
rw [←zero_eq, zero_add, add_zero]
State after:
no goals

State before:
x y : Nat
ih : x + y = y + x
⊢ x + succ y = succ y + x
Tactic:
sorry
State after:
no goals