MobiusLemma.sum_moebius_div_sq

theorem sum_moebius_div_sq : ∑' n, (moebius n) / (n : ℝ) ^ 2 = 1 / (riemannZeta 2).re := by  have h_sum : ∑' n, (moebius n) / (n : ℂ) ^ 2 = 1 / riemannZeta 2 := by    have h_zeta2 : riemannZeta 2 * ∑' n, (moebius n : ℂ) / (n : ℂ) ^ 2 = 1 := by      convert LSeries_zeta_mul_Lseries_moebius (show 1 < (2 : ℂ).re by norm_num) using 1      norm_num [LSeries]; congr! 1      · rw [zeta_eq_tsum_one_div_nat_cpow] <;> norm_num [LSeries.term]        exact tsum_congr fun n ↦ by aesop      · norm_num [LSeries.term]; exact tsum_congr fun n ↦ by aesop    exact eq_one_div_of_mul_eq_one_right h_zeta2  convert congr_arg re h_sum using 1  · rw_mod_cast [re_tsum]    · rfl    · contrapose! h_sum      rw [tsum_eq_zero_of_not_summable h_sum]; norm_num [riemannZeta_two]      exact (div_ne_zero (by norm_num)        (pow_ne_zero 2 (ofReal_ne_zero.mpr Real.pi_ne_zero))).symm  · norm_num [normSq, div_re]    rw [inv_eq_one_div, div_eq_div_iff] <;> norm_num [riemannZeta_two]    · norm_cast    · norm_cast; positivity    · norm_cast; positivity