ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ (i : ι), g * h i
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h
rw [mul_iInf]
no goals
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ (i : ι), g * h i
exact le_ciInf H