Theorem: int_sum_nat
Proof state before:
case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0 =
    f ↑N.succ + f (-Int.ofNat N.succ) + (∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0)

case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ -Int.ofNat N.succ ∉ Icc (-Int.ofNat N) ↑N

case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)
Tactic:
rw [sum_range_succ, add_comm, ←add_assoc, add_comm]
Proof state after:
case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ f ↑(N + 1) + f (-↑(N + 1)) + (-f 0 + ∑ x ∈ range (N + 1), (f ↑x + f (-↑x))) =
    f ↑N.succ + f (-Int.ofNat N.succ) + (∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0)

case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ -Int.ofNat N.succ ∉ Icc (-Int.ofNat N) ↑N

case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)