no goals
α : Type ?u.131868
β : Type ?u.131871
γ : Type ?u.131874
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ (a + ⨆ (i : ι) (_ : p i), f i) = ⨆ (i : ι) (_ : p i), a + f i
simp only [add_comm a, biSup_add' h]