have : (d^2:ℝ) ≤ (d*m)^2 := by
  norm_cast;
  refine Nat.pow_le_pow_of_le_left ?h 2
  exact Nat.le_mul_of_pos_right _ (Nat.pos_of_mem_divisors hm)
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ False
case pos.h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
this : ↑d ^ 2 ≤ (↑d * ↑m) ^ 2
⊢ False