rw [hr, Nat.gcd_mul_left, mul_eq_left₀ hk, Nat.gcd_comm]
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ d.gcd (k * m) = k
case intro.a
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
hrdvd : r ∣ d
⊢ m.gcd r = 1