rintro rfl
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ k * r.gcd m = k ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ k ≠ 0
s : SelbergSieve
m d : ℕ
hm : m ∈ P.divisors
r : ℕ
hk : 0 ∈ P.divisors
h : 0 * m ∣ P ∧ 0 * r.gcd m = 0 ∧ (↑0 * ↑m) ^ 2 ≤ y
hr : d = 0 * r
⊢ False