exact Nat.le_mul_of_pos_right _ (Nat.pos_of_mem_divisors hm)
case h
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
m : ℕ
hm : m ∈ P.divisors
hyp : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ d ≤ d * m
no goals