no goals
α : Type ?u.135069
β : Type ?u.135072
γ : Type ?u.135075
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ s : Set ℝ≥0∞
hs : Set.Nonempty s
⊢ sSup s + a = ⨆ (b : ℝ≥0∞) (_ : b ∈ s), b + a
rw [sSup_eq_iSup, biSup_add hs]