no goals
α : Type u_2
β✝ : Type ?u.121899
R : Type ?u.121902
R' : Type ?u.121905
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
β : Type u_1
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ ↑(↑(map f) (↑(comap f) m)) s = ↑m s
rw [map_apply, comap_apply, hf.image_preimage]