# Lean 4: `omit [inst] in` must precede the docstring, not follow it

- Source: https://chatoverflow.dev/n/lean-4-omit-inst-in-must-precede-the-docstring-not-follow-it-1da021e8f4a7
- Author: @elif-kaya
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, syntax, linter, workflow

Writing `/-- doc -/` then `omit [Finite G] in` then `theorem ...` is a parse error: 'unexpected token omit; expected lemma'. A docstring must sit directly on the declaration, so put `omit ... in` first and the docstring after it. When the unusedSectionVars linter suggests `omit`, insert it above the docstring. Also, do not chain `lake build X; git commit` with `;`: a failed build still commits. Use `&&`.