Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
These are non-negotiable constraints for writing Lean proofs correctly.
Write one tactic, check diagnostics (use done to see unsolved goals), repeat. Never write multiple tactics before checking.
by sorry is acceptable: For placeholders you're not actively working on.
done is required: When you expect there to be next steps in an active proof.
Fix errors in this order — higher-priority errors make lower-priority ones unreliable:
"Unsolved goals" errors appear on by or => lines, NOT where you add tactics. If there's an "unsolved goals" on line 59 but a tactic error on line 65 — fix line 65 FIRST.
Stop writing tactics after any error.
Go directly to the target theorem. Don't fill in sorrys in helper lemmas first — Lean treats sorry as an axiom, so dependent theorems still work.
Move sorries earlier in the file by replacing a sorry proof with references to simpler lemmas:
-- Before:
theorem main_theorem : A = C := by sorry
-- After:
theorem lemma1 : A = B := by sorry
theorem lemma2 : B = C := by sorry
theorem main_theorem : A = C := by
rw [lemma1, lemma2]
When a proof has multiple cases, sorry the easy cases and work on the hardest one first. If the hard case fails, effort on easy cases is wasted.
match n with
| 0 => sorry -- fill in later
| 1 => sorry -- fill in later
| n + 2 => -- WORK ON THIS FIRST
After getting a proof to work, clean it up immediately:
rw [a]; rw [b] → rw [a, b])simp can handle more (remove earlier steps one by one)When you encounter "motive is not type correct" or similar errors during rewriting:
Rewriting a term b that appears in dependent types (like hab : a ≤ b) fails because the motive cannot abstract over the dependencies.
have hb : b = f x
rw [hb] -- Error: motive is not type correct
Prove a generalized statement for an arbitrary parameter, then instantiate:
suffices ∀ s, statement_about s by
have h_specific := the_equality_you_have
convert this ?_ <;> exact h_specific
intro s
-- Now prove the general statement for arbitrary s
This works because the generalized statement has no dependencies on the problematic term, and convert handles the dependent type coercions at the end.
Never declare a proof complete while sorry placeholders or error diagnostics remain.