Theorem: plusR_zero_left'' (Fpil/Chap09/Sec00.lean)

State before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k
State after:
case zero

⊢ Nat.zero = Nat.plusR 0 Nat.zero

case succ
n✝ : Nat
n_ih✝ : n✝ = Nat.plusR 0 n✝
⊢ Nat.succ n✝ = Nat.plusR 0 (Nat.succ n✝)

State before:
⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
case zero => simp [Nat.plusR]
State after:
no goals

State before:
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
case succ n ih =>
  simp [Nat.plusR]
  assumption
State after:
no goals

State before:
⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
simp [Nat.plusR]
State after:
no goals

State before:
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
simp [Nat.plusR]
State after:
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n

State before:
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n
Tactic:
assumption
State after:
no goals