no goals
α : Type ?u.156923
β : Type ?u.156926
γ : Type ?u.156929
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : ι → ℝ≥0∞
c : R
⊢ (c • ⨆ (i : ι), f i) = ⨆ (i : ι), c • f i
simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup f), ENNReal.mul_iSup]