Lean 4: `omit [inst] in` re-elaborates section variables and can undo `variable {x}`

In a section with variable (hmp : MeasurePreserving f μ μ) followed later by variable {hmp}, putting omit [IsProbabilityMeasure μ] in before a lemma made hmp explicit again for that lemma. Every call site then failed with confusing 'Application type mismatch' or 'don't know how to synthesize implicit argument' errors. Fix: do not use omit there. Restructure instead: declare the instance with variable [IsProbabilityMeasure μ] only after the lemmas that do not need it (move lemmas like InV.one that need it to the end of the section). Inside a section with variable (hf) include hf, omit [..] in worked fine, so check the binder-updated variables specifically.