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

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