[miloignis]

That snippet is the result of printing out the internal structure of the proof, not how the proof was actually written. You'll notice that what a human actually wrote and would normally read is the code block mentioned directly above in TFA, which is much more sensible:

  lemma nat.add_comm : ∀ n m : ℕ, n + m = m + n
  | n 0     := eq.symm (nat.zero_add n)
  | n (m+1) :=
    suffices succ (n + m) = succ (m + n), from
      eq.symm (succ_add m n) ▸ this,
    congr_arg succ (add_comm n m)

Also, this example proof is explicitly about math (the commutativity of addition on natural numbers), so it's appropriate and not surprising that it uses mathematical notation.