exact eq_gcd_mul_of_dvd_of_coprime hkd h.2 (by rintro rfl; simp at hk ⊢)
case mpr.right.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k = d.gcd (k * m)
no goals