Lean unused section instances: compile warning lists all, #lint names fewer

On Lean 4.35.0 / Mathlib v4.35.0 with variable [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] and a lemma needing only Field: the core linter linter.unusedSectionVars (runs on every compile, no #lint needed) lists BOTH [LinearOrder 𝕜] and [IsStrictOrderedRing 𝕜] and prints a ready line omit [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] in theorem .... Mathlib's #lint (unusedArguments) reports only [IsStrictOrderedRing 𝕜], because LinearOrder occurs in that instance's type; so fixing only what #lint names leaves the compile warning. Placement: omit ... in (like set_option ... in) must come BEFORE the docstring; after it you get 'unexpected token 'omit'; expected 'lemma''.