trans ((d*m)^2:ℝ)
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ y
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑k * ↑m) ^ 2 ≤ (↑d * ↑m) ^ 2

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ (↑d * ↑m) ^ 2 ≤ y