Mertens.tsum_M_eq_f_eq_tsum

lemma tsum_M_eq_f_eq_tsum :    -∑' (n : ℕ), M_eq_f n = ∑' p : ℕ, if p.Prime then log (1 - 1 / p) + 1 / p else 0 := by  rw [tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers M_eq_f.HasSum.summable    (fun n hn ↦ (by simp_all [vonMangoldt_ne_zero_iff])), M_eq_f.sum_primes, zero_add,    tsum_primes_eq_tsum_ite (fun p ↦ ∑' (k : ℕ), M_eq_f (p ^ (k + 2))), ← tsum_neg]  refine tsum_congr fun n ↦ ?_  split_ifs with hn  · rw [← HasSum_log_one_sub_one_div_prime hn|>.tsum_eq, HasSum_log_one_sub_one_div_prime hn|>.summable.tsum_eq_zero_add]    simp only [ite_not, Nat.cast_pow, log_pow, Nat.cast_add, Nat.cast_ofNat, CharP.cast_eq_zero,      zero_add, pow_one, one_mul, Nat.cast_one, one_div]    trans -∑' (k : ℕ), (1 : ℝ) / ((k + 2) * n ^ (k + 2))    · congr      ext k      have : ¬(Nat.Prime (n ^ (k + 2))) := by exact Nat.Prime.not_prime_pow (by grind)      simp only [this, ↓reduceIte, one_div, mul_inv_rev]      rw [vonMangoldt_apply_pow (by grind), vonMangoldt_apply_prime hn]      have : log n ≠ 0 := by simp; grind [hn.two_le]      field    · rw [← tsum_neg]      ring_nf      congr      ext      ring_nf  · ring