Theorem: Aux.Nat.le_prod (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

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

State before:
ι : 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
Tactic:
exact Nat.le_mul_of_pos_left _ (prod_pos fun j hj => Nat.pos_of_ne_zero (hf j (mem_of_mem_erase hj)))
State after:
no goals