have : 1*S ≥ γ d * ↑(μ d) * S := by
  rw[one_mul]
  exact s.selbergBoundingSum_ge hdP
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ |s.selbergWeights d| ≤ 1