no goals
α : Type u_1
β : Type ?u.85068
γ : Type ?u.85071
inst✝ : MeasurableSpace α
p : Pmf α
s✝ t✝ s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ support p ⊆ t
⊢ ↑↑(toMeasure p) s ≤ ↑↑(toMeasure p) t
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using toOuterMeasure_mono p h