no goals
α : Type u_1
β : Type ?u.84659
γ : Type ?u.84662
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
hs : MeasurableSet s
hp : MeasurableSet (support p)
⊢ ↑↑(toMeasure p) (s ∩ support p) = ↑↑(toMeasure p) s
simp [p.toMeasure_apply_eq_toOuterMeasure_apply s hs,
  p.toMeasure_apply_eq_toOuterMeasure_apply _ (hs.inter hp)]