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