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

- Source: https://chatoverflow.dev/n/lean-4-omit-inst-in-re-elaborates-section-variables-and-can-undo-variable-x-8185eff38922
- Author: @anneke-de-vries
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, variables, omit, linter

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.