rw [← abs_of_nonneg <| s.selbergWeights_mul_mu_nonneg d hdP,
  abs_mul, ←Int.cast_abs, abs_moebius_eq_one_of_squarefree <|
  (s.prodPrimes_squarefree.squarefree_of_dvd hdP), Int.cast_one, mul_one]
case h.e'_3
s : SelbergSieve
d : ℕ
hdP : d ∣ P
this : s.selbergWeights d * ↑(μ d) ≤ 1
⊢ |s.selbergWeights d| = s.selbergWeights d * ↑(μ d)
no goals