no goals
α : Type u_3
β : Type ?u.70023
R : Type u_1
R' : Type ?u.70029
ms : Set (OuterMeasure α)
m : OuterMeasure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
ι : Sort u_2
f : ι → OuterMeasure α
c : R
s : Set α
⊢ ↑(c • ⨆ (i : ι), f i) s = ↑(⨆ (i : ι), c • f i) s
simp only [smul_apply, iSup_apply, ENNReal.smul_iSup]