∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α}
  (f : α → MeasureTheory.Measure β) {s : Set β}, MeasurableSet s → (m.bind f) s ≤ ∫⁻ (a : α), (f a) s ∂m