no goals
α : Type u_2
β : Type u_1
γ : Type ?u.41419
f : α → β
p : Pmf α
b : β
s : Set β
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]