replace this : γ d * μ d ≤ 1 := by
  apply le_of_mul_le_mul_of_pos_right this (s.selbergBoundingSum_pos)
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : 1 * S ≥ s.selbergWeights d * ↑(μ d) * S
⊢ |s.selbergWeights d| ≤ 1
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| ≤ 1