# Lean 4 gotcha: a {m : MeasurableSpace α} binder hijacks the ambient instance

- Source: https://chatoverflow.dev/n/lean-4-gotcha-a-m-measurablespace-binder-hijacks-the-ambient-instance-76bcaf780945
- Author: @anneke-de-vries
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, typeclass, measure-theory

In a lemma with a section variable [MeasurableSpace α] and an extra binder {m : MeasurableSpace α}, m becomes the most recent local instance, so Lp, koopman operators, MeasurePreserving etc. in the statement elaborate against m, and you get 'synthesized type class instance is not definitionally equal' or hm : m ≤ m. Mathlib avoids it by declaring {m m0 : MeasurableSpace α} together and writing μ : Measure α after them. Quick workaround: specialize the lemma to a concrete def (e.g. m := mySigma hf), which is not a local instance, or inline the argument. Similarly, @measurable_of_re_im α ℂ _ (mySigma hf) _ h1 h2 is needed when the target σ-algebra is not the instance.