case pos
α : Type ?u.866567
β : Type ?u.866570
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort ?u.866587
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
h0 : x = 0
⊢ iInf f * x = ⨅ (i : ι), f i * x

case neg
α : Type ?u.866567
β : Type ?u.866570
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort ?u.866587
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
h0 : ¬x = 0
⊢ iInf f * x = ⨅ (i : ι), f i * x
α : Type ?u.866567
β : Type ?u.866570
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort ?u.866587
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
⊢ iInf f * x = ⨅ (i : ι), f i * x
by_cases h0 : x = 0
no goals
case pos
α : Type ?u.866567
β : Type ?u.866570
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort ?u.866587
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
h0 : x = 0
⊢ iInf f * x = ⨅ (i : ι), f i * x
simp only [h0, mul_zero, iInf_const]
no goals
case neg
α : Type ?u.866567
β : Type ?u.866570
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort ?u.866587
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
h0 : ¬x = 0
⊢ iInf f * x = ⨅ (i : ι), f i * x
exact iInf_mul_of_ne h0 h