Proving · 7 min

Equality proofs

A proposition is a type in Prop. A proof is a term of that type. A theorem declaration gives the proof a name, states its proposition after :, and supplies the proof term after :=.

by starts a tactic proof. rfl stands for reflexivity: a value equals itself (x = x). Lean can unfold definitions and compute to check that both sides reduce to the same expression. For example, rfl proves 2 + 2 = 4 because both sides reduce to 4.

Exercise

Replace sorry with a proof of 3 + 4 = 7.

theorem seven : 3 + 4 = 7 := by
  sorry

theorem seven : 3 + 4 = 7 := by
  rfl

Related example