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

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.