no goals
α : Type u_1
β : Type u_2
R : Type ?u.126810
R' : Type ?u.126813
ms : Set (OuterMeasure α)
m : OuterMeasure α
f : α → β
s : Set α
hs : Set.Nonempty s
⊢ ↑(↑(comap f) ⊤) s = ↑⊤ s
rw [comap_apply, top_apply hs, top_apply (hs.image _)]