no goals
α : Type u_2
β✝ : Type ?u.123348
R : Type ?u.123351
R' : Type ?u.123354
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
β : Type u_1
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
⊢ ↑(↑(comap f) (↑(map f) m)) s = ↑m s
rw [comap_apply, map_apply, hf.preimage_image]