no goals
α : Type u_2
β : Type ?u.105796
R : Type ?u.105799
R' : Type ?u.105802
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Sort u_1
s : Set α
m : ι → OuterMeasure α
⊢ ↑(restrict s) (⨆ (i : ι), m i) = ⨆ (i : ι), ↑(restrict s) (m i)
simp [restrict]