case h
α : Type u_1
β : Type ?u.40352
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(bind m dirac) s = ↑↑m s
α : Type u_1
β : Type ?u.40352
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
⊢ bind m dirac = m
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.40352
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(bind m dirac) s = ↑↑m s
simp only [bind_apply hs measurable_dirac, dirac_apply' _ hs, lintegral_indicator 1 hs,
  Pi.one_apply, lintegral_one, restrict_apply, MeasurableSet.univ, univ_inter]