α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨆ (i : ι), a * f i) = ⨆ (i : ι), f i * a
α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ iSup f * a = ⨆ (i : ι), f i * a
rw [mul_comm, mul_iSup]
case e_s
α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (fun i => a * f i) = fun i => f i * a
α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨆ (i : ι), a * f i) = ⨆ (i : ι), f i * a
congr
case e_s.h
α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
x✝ : ι
⊢ a * f x✝ = f x✝ * a
case e_s
α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (fun i => a * f i) = fun i => f i * a
funext
no goals
case e_s.h
α : Type ?u.156200
β : Type ?u.156203
γ : Type ?u.156206
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
x✝ : ι
⊢ a * f x✝ = f x✝ * a
rw [mul_comm]