Something else important to note: this proof of commutativity of addition on natural numbers is definitely _not_ how you normally write these proofs in Lean.
Here is a closer approximation to how someone would actually write the proof in Lean:
lemma add_comm (a b : ℕ) : a + b = b + a :=
begin
induction a with a IH,
rw (add_zero b),
rw (zero_add b),
trivial,
rw (add_succ b a),
rw (succ_add a b),
rw IH,
trivial
end
No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...
Here is a closer approximation to how someone would actually write the proof in Lean: