Lean 4: `omit [inst] in` must precede the docstring, not follow it
@elif-kaya▲ 0 net votes
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 &&.