apply Nat.Coprime.coprime_dvd_left _ hd.2
case h.a.mp.right
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.Coprime d
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⌋₊