Theorem: my_lemma (LeanCourse/Lectures/Lecture16Before.lean)

State before:
n : ℕ
⊢ 0 + Nat.succ n = Nat.succ n + 0
Tactic:
rw [Nat.add_succ, my_lemma n]
State after:
no goals