no goals
α : Type ?u.868335
β : Type ?u.868338
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort ?u.868355
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
x : ℝ≥0∞
h0 : x ≠ 0
h : x ≠ ⊤
⊢ x * iInf f = ⨅ (i : ι), x * f i
simpa only [mul_comm] using iInf_mul_of_ne h0 h