no goals
α : Type u_2
β : Type u_1
R : Type ?u.127541
R' : Type ?u.127544
ms : Set (OuterMeasure α)
m : OuterMeasure α
f : α → β
s : Set β
⊢ ↑(↑(map f) ⊤) s = ↑(↑(restrict (range f)) ⊤) s
rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
  Set.image_eq_empty]