Theorem: Sieve.prod_primes_dvd_of_dvd (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
P : ℕ
s : Finset ℕ
h : ∀ p ∈ s, p ∣ P
h' : ∀ p ∈ s, p.Prime
⊢ ∏ p ∈ s, p ∣ P
Tactic:
simp_rw [Nat.prime_iff] at h'
State after:
P : ℕ
s : Finset ℕ
h : ∀ p ∈ s, p ∣ P
h' : ∀ p ∈ s, Prime p
⊢ ∏ p ∈ s, p ∣ P

State before:
P : ℕ
s : Finset ℕ
h : ∀ p ∈ s, p ∣ P
h' : ∀ p ∈ s, Prime p
⊢ ∏ p ∈ s, p ∣ P
Tactic:
apply Finset.prod_primes_dvd _ h' h
State after:
no goals