Nitpick, but it's a bit strange to say that the two_eq_two theorem looks like a function. It looks more like a constant, since it has no arguments. (Yes I know that constants are nullary functions.)

I would find the following a more convincing presentation:

    theorem x_eq_x (x:nat) : x = x := by
      rfl

    theorem 2_eq_2 : 2 = 2 := by
      exact (x_eq_x 2)

Fair! I decided not to do that because the way arguments work (and dependent types in general — like being able to return a proof of `x = x` given x) is unusual for people like me, and deserves an article of its own. So I’m kicking that to one of the next articles.