α : Type ?u.136001
β : Type ?u.136004
γ : Type ?u.136007
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
ι : Sort u_1
s : ι → ℝ≥0∞
inst✝ : Nonempty ι
⊢ (⨆ (b : ι), s b + a) = ⨆ (b : ι), a + s b
α : Type ?u.136001
β : Type ?u.136004
γ : Type ?u.136007
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
ι : Sort u_1
s : ι → ℝ≥0∞
inst✝ : Nonempty ι
⊢ a + iSup s = ⨆ (b : ι), a + s b
rw [add_comm, iSup_add]
no goals
α : Type ?u.136001
β : Type ?u.136004
γ : Type ?u.136007
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
ι : Sort u_1
s : ι → ℝ≥0∞
inst✝ : Nonempty ι
⊢ (⨆ (b : ι), s b + a) = ⨆ (b : ι), a + s b
simp [add_comm]