ZetaAppendix.hsummable''

lemma hsummable'' {z : ℂ} (hz : z ∈ integerComplement) :    Summable fun n : ℕ+ ↦ 1 / (z - (2 * n - 1)) + 1 / (z + (2 * n - 1)) := by  have he (n : ℕ+) := cotTerm_identity hz (2 * n - 2)  have hi : (fun n : ℕ+ ↦ (2 * n - 1 : ℤ)).Injective := fun _ _ _ ↦ by simp_all  have := mul_left (2 * z)    ((EisensteinSeries.summable_linear_sub_mul_linear_add z 1 1).comp_injective hi)  have (n : ℕ+) : ((2 * n - 2 : ℕ) : ℂ) + 1 = ((2 * n : ℕ) : ℂ) - 1 := by    norm_cast    rw [Nat.cast_add, Int.subNatNat_eq_coe, Nat.cast_sub] <;> push_cast <;> linarith [n.pos]  simp_all [cotTerm, mul_comm (z + _)⁻¹]