cases' hkd with r hr
case mp.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ m.Coprime d
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
r : ℕ
hr : d = k * r
⊢ m.Coprime d