Plan a proof, then fill it in

Longer proofs are easier to write in two passes. First write the structure: the intro, the obtain, the constructor and one bullet per branch. Then fill in the branches one at a time. sorry is what makes the first pass possible: it closes any goal without proving it, as a placeholder.

Lean still checks everything around a sorry. If the skeleton itself is wrong, say you split a goal that is not a conjunction, you find out immediately instead of after writing every branch. A file that uses sorry compiles with the warning declaration uses 'sorry', and an Academy exercise never counts as complete while one is left.

To see what a hole still needs, replace its sorry with skip, which does nothing. Lean then reports unsolved goals for that bullet and prints the goal, with its hypotheses above the line. Fill in the proof there, check again, and move to the next hole.

This is how people work in real Lean projects as well: sketch the argument with holes, confirm that the outline compiles, and make the holes smaller until none are left.

Worked example

example (A B : Prop) (ha : A) (hb : B) : B ∧ A := by
  constructor
  · exact hb
  · exact ha

-- The same proof halfway through, with one hole left:
--   constructor
--   · exact hb
--   · sorry
--
--   warning: declaration uses 'sorry'
--
-- With `skip` in place of `sorry`, Lean shows what the hole needs:
--   error: unsolved goals
--   case right
--   A B : Prop
--   ha : A
--   hb : B
--   ⊢ A

The finished proof is on top; the comments show the two messages you see on the way there. case right names the branch: the right half of the conjunction.