no goals
α : Type ?u.155493
β : Type ?u.155496
γ : Type ?u.155499
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ a * sSup s = ⨆ (i : ℝ≥0∞) (_ : i ∈ s), a * i
simp only [sSup_eq_iSup, mul_iSup]