completedRiemannZeta_two

theorem completedRiemannZeta_two :    completedRiemannZeta (2 : ℂ) = (Real.pi : ℂ) / 6 := by  have hs : (1 : ℝ) < Complex.re (2 : ℂ) := by norm_num  have hpi0 : (Real.pi : ℂ) ≠ 0 := by exact_mod_cast Real.pi_ne_zero  have htsum :      completedRiemannZeta (2 : ℂ) = (Real.pi : ℂ)⁻¹ * (∑' n : ℕ, ((n : ℂ) ^ 2)⁻¹) := by    simpa [Complex.cpow_neg_one] using      (completedZeta_eq_tsum_of_one_lt_re (s := (2 : ℂ)) hs)  have hzeta : riemannZeta (2 : ℂ) = ∑' n : ℕ, ((n : ℂ) ^ 2)⁻¹ := by    simpa using (zeta_eq_tsum_one_div_nat_cpow (s := (2 : ℂ)) hs)  have hζ2 : riemannZeta (2 : ℂ) = (Real.pi : ℂ) ^ 2 / 6 := by    simpa using (riemannZeta_two : riemannZeta (2 : ℂ) = (Real.pi : ℂ) ^ 2 / 6)  have hΛ2' : completedRiemannZeta (2 : ℂ) = (Real.pi : ℂ)⁻¹ * riemannZeta (2 : ℂ) := by    simpa [hzeta] using htsum  calc    completedRiemannZeta (2 : ℂ)        = (Real.pi : ℂ)⁻¹ * ((Real.pi : ℂ) ^ 2 / 6) := by            simpa [hζ2] using hΛ2'    _ = (Real.pi : ℂ) / 6 := by            field_simp [hpi0]