exact ⟨h.2.2, coprime_of_squarefree_mul $ Squarefree.squarefree_of_dvd h.1 s.prodPrimes_squarefree⟩
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : d * m ∣ P ∧ d ∣ d * m ∧ (↑d * ↑m) ^ 2 ≤ y
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
no goals