SelbergSieve.selbergWeights_eq_dvds_sum

theorem selbergWeights_eq_dvds_sum (d : ℕ) :    ν d * γ d =      S⁻¹ * μ d *        ∑ l ∈ divisors P, if d ∣ l ∧ l ^ 2 ≤ y then g l else 0 := by  by_cases h_dvd : d ∣ P  swap  · dsimp only [selbergWeights]; rw [if_neg h_dvd]    rw [sum_eq_zero]    · ring    intro l hl; rw [mem_divisors] at hl    rw [if_neg]; push Not; intro h    exfalso; exact h_dvd (dvd_trans h hl.left)  dsimp only [selbergWeights]  rw [if_pos h_dvd]  repeat rw [mul_sum]  -- change of variables l=m*d  apply symm  rw [sum_mul_subst d P]  · apply sum_congr rfl    intro m hm    rw [mul_ite_zero, ←ite_and, mul_ite_zero, mul_ite_zero]    apply if_ctx_congr _ _ fun _ => rfl    · rw [coprime_comm]      constructor      · intro h        push_cast at h        exact ⟨h.2.2, coprime_of_squarefree_mul          <| Squarefree.squarefree_of_dvd h.1 s.prodPrimes_squarefree⟩      · intro h        push_cast        exact ⟨ Coprime.mul_dvd_of_dvd_of_dvd h.2 h_dvd (dvd_of_mem_divisors hm),          Nat.dvd_mul_right d m, h.1⟩    · intro h      trans ((ν d)⁻¹ * (ν d) * g d * μ d / S * g m)      · rw [inv_mul_cancel₀ (nu_ne_zero h_dvd),          (selbergTerms_mult _).map_mul_of_coprime <| coprime_comm.mp h.2]        ring      ring  · intro l _ hdl    rw [if_neg, mul_zero]    push Not; intro h; contradiction