no goals
α : Type u_2
β✝ : Type ?u.78827
R : Type ?u.78830
R' : Type ?u.78833
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
β : Type u_1
f : α → β
m m' : OuterMeasure α
s : Set β
⊢ ↑(↑(map f) (m ⊔ m')) s = ↑(↑(map f) m ⊔ ↑(map f) m') s
simp only [map_apply, sup_apply]