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

State before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k with
| zero => rfl
| succ n ih =>
  simp [Nat.plusR]
  assumption
State after:
no goals

State before:
case zero

⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
rfl
State after:
no goals

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

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