no goals
α : Type u_1
β : Type ?u.83685
γ : Type ?u.83688
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
a : α
h : MeasurableSet {a}
⊢ ↑↑(toMeasure p) {a} = ↑p a
simp [toMeasure_apply_eq_toOuterMeasure_apply _ _ h, toOuterMeasure_apply_singleton]