rw [←prod_erase_mul (a:=i) (h:= hi)]
ι : Type u_1
inst✝ : DecidableEq ι
f : ι → ℕ
s : Finset ι
i : ι
hi : i ∈ s
hf : ∀ i ∈ s, f i ≠ 0
⊢ f i ≤ ∏ j ∈ s, f j
ι : 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