no goals
α : Type ?u.118140
β : Type ?u.118143
γ : Type ?u.118146
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
⊢ (⨅ (i : ι), f i * a) = (⨅ (i : ι), f i) * a
simpa only [mul_comm a] using iInf_mul_left' h h0