no goals
α : Type u_1
β : Type u_2
R : Type ?u.128472
R' : Type ?u.128475
ms : Set (OuterMeasure α)
m : OuterMeasure α
f : α → β
hf : Surjective f
⊢ ↑(map f) ⊤ = ⊤
rw [map_top, hf.range_eq, restrict_univ]