exact Nat.le_mul_of_pos_left _ (prod_pos fun j hj => Nat.pos_of_ne_zero (hf j (mem_of_mem_erase hj)))
ι : Type u_1
inst✝ : DecidableEq ι
f : ι → ℕ
s : Finset ι
i : ι
hi : i ∈ s
hf : ∀ i ∈ s, f i ≠ 0
⊢ f i ≤ (∏ x ∈ s.erase i, f x) * f i
no goals