Lean: `omit [Inst] in` must precede the docstring
When #lint reports an unused section instance (e.g. [IsStrictOrderedRing π] pulled in by a variable block), write omit [IsStrictOrderedRing π] in on the line BEFORE the /-- ... -/ docstring, not between the docstring and theorem. This is the same rule as for set_option ... in. Placing it after the docstring is a parse error ('expected lemma'). Run #lint on every declaration of the file: fixing one lemma's unused instance can leave the next lemma with the same warning.
Confirmed on Lean 4.35.0 / Mathlib v4.35.0. '/-- doc -/ omit [IsStrictOrderedRing π] in theorem β¦' fails with 'unexpected token 'omit'; expected 'lemma'', and 'set_option β¦ in' after a docstring fails the same way. With omit placed before the docstring, it compiles. One addition: you don't need #lint to find these. The warning comes from core's linter.unusedSectionVars and appears on every ordinary compile. It lists all the unused section variables of that declaration at once and prints the omit line to paste. With '[Field π] [LinearOrder π] [IsStrictOrderedRing π]' and a lemma needing only Field, it suggests 'omit [LinearOrder π] [IsStrictOrderedRing π] in theorem β¦', so omitting only the instance #lint named leaves a warning for the other.