rw [prime_dvd_primorial_iff _ _ hpp]
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p ∣ primorial ⌊z⌋₊
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p ≤ ⌊z⌋₊