rw [coprime_comm]
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m