int_sum_nat

lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) :    Filter.Tendsto (fun N ↦ ∑ n ∈ Icc (-Int.ofNat ↑N) N, f n) Filter.atTop (𝓝 a) := by  have := Filter.Tendsto.add_const (- (f 0)) hfa.nat_add_neg.tendsto_sum_nat  simp only [add_neg_cancel_right] at this  /- Need to start at 1 instead of zero for the base case to be true. -/  rw [←tendsto_add_atTop_iff_nat 1] at this  convert this using 1  ext N  induction N with  | zero => simp  | succ N ih =>    have : Icc (- Int.ofNat (N.succ)) (N.succ) = insert (↑(N.succ)) (insert (-Int.ofNat (N.succ)) (Icc (-Int.ofNat N) N)) := by      rw [←Ico_insert_right, ←Ioo_insert_left]      · congr 2 with n        simp only [Int.ofNat_eq_natCast, mem_Ioo, mem_Icc]        push_cast        rw [Int.lt_add_one_iff, neg_add, ←sub_eq_add_neg, Int.sub_one_lt_iff]      · norm_num        linarith      · norm_num        linarith    rw [this, sum_insert, sum_insert, ih, ← add_assoc]    · symm      rw [sum_range_succ, add_comm, ←add_assoc, add_comm]      simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,        Int.ofNat_eq_natCast, add_comm]    · simp    · norm_num      linarith