no goals
α : Type u_3
β✝ : Type ?u.94749
R : Type ?u.94752
R' : Type ?u.94755
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
β : Type u_1
ι : Sort u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
⊢ ↑(↑(comap f) (⨆ (i : ι), m i)) s = ↑(⨆ (i : ι), ↑(comap f) (m i)) s
simp only [comap_apply, iSup_apply]