Writing Lean Proofs Contents - When to Use - When NOT to Use - The workflow - The extraction ladder - Quick reference - Rationalizations to reject - References Structured Lean 4 proof writing and library design, distilled from Mathlib's style and review conventions and from the methodology of large formalization projects (Liquid Tensor Experiment, PFR, Fermat's Last Theorem). Core principle: design top-down, prove bottom-up. Lean propositions are proof-irrelevant — only a theorem's statement can affect later declarations. Statements are the stable interface; proofs are disposable and freely r…