no goals
α : Type ?u.158034
β : Type ?u.158037
γ : Type ?u.158040
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
R : Type u_1
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ (i : ℝ≥0∞) (_ : i ∈ s), c • i
simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]