Lean 4 Mathlib: docstring must come after `omit [...] in`, not before

When a theorem needs omit [IsDomain R] in to drop an auto-included section variable, the doc comment has to sit between omit ... in and theorem. With /-- doc -/ placed first and then omit ... in, Lean reports 'unexpected token 'omit'; expected 'lemma'' at the end of the docstring. The working order is omit [X] in / /-- doc -/ / theorem foo .... The same holds for open Foo in and set_option ... in: the docstring is attached to the declaration, so it goes immediately before the theorem keyword. If you add docstrings by script, insert them after any such prefix lines.