SelbergSieve.selbergWeights_diagonalisation

theorem selbergWeights_diagonalisation (l : ℕ) (hl : l ∈ divisors P) :    (∑ d ∈ divisors P, if l ∣ d then ν d * γ d else 0) =      if l ^ 2 ≤ y then g l * μ l * S⁻¹ else 0 := by  calc    (∑ d ∈ divisors P, if l ∣ d then ν d * γ d else 0) =        ∑ d ∈ divisors P, ∑ k ∈ divisors P,          if l ∣ d ∧ d ∣ k ∧ k ^ 2 ≤ y then g k * S⁻¹ * (μ d:ℝ) else 0 := by      apply sum_congr rfl; intro d _      rw [selbergWeights_eq_dvds_sum, ← boole_mul, mul_sum, mul_sum]      apply sum_congr rfl; intro k _      rw [mul_ite_zero, ite_zero_mul_ite_zero]      apply if_ctx_congr Iff.rfl _ (fun _ => rfl);      intro _; ring    _ = ∑ k ∈ divisors P, if k ^ 2 ≤ y then            (∑ d ∈ divisors P, if l ∣ d ∧ d ∣ k then (μ d:ℝ) else 0) * g k * S⁻¹          else 0 := by      rw [sum_comm]; apply sum_congr rfl; intro k _      apply symm      rw [← boole_mul, sum_mul, sum_mul, mul_sum, sum_congr rfl]      intro d _      rw [ite_zero_mul, ite_zero_mul, ite_zero_mul, one_mul, ←ite_and]      apply if_ctx_congr _ _ (fun _ => rfl)      · tauto      intro _; ring    _ = if l ^ 2 ≤ y then g l * μ l * S⁻¹ else 0 := by      rw [← sum_ite_eq_of_mem' (divisors P) l (fun _ => if l^2 ≤ y then g l * μ l * S⁻¹ else 0) hl]      apply sum_congr rfl; intro k hk      rw [Aux.moebius_inv_dvd_lower_bound_real s.prodPrimes_squarefree l _ (dvd_of_mem_divisors hk),        ←ite_and, ite_zero_mul, ite_zero_mul, ← ite_and]      apply if_ctx_congr _ _ fun _ => rfl      · rw [and_comm, eq_comm]; apply and_congr_right        intro heq; rw [heq]      · intro h; rw [h.1]; ring