Theorem: int_sum_nat (Carleson/Theorem1_1/Approximation.lean)

State before:
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
have := hfa.nat_add_neg.tendsto_sum_nat
State after:
β : 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))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)

State before:
β : 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))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
have := (Filter.Tendsto.add_const (- (f 0))) this
State after:
β : 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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 (a + f 0 + -f 0))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)

State before:
β : 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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 (a + f 0 + -f 0))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
simp at this
State after:
β : 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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)

State before:
β : 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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
rw [←tendsto_add_atTop_iff_nat 1] at this
State after:
β : 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)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)

State before:
β : 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)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
convert this using 1
State after:
case h.e'_3
β : 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)
⊢ (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) = fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0

State before:
case h.e'_3
β : 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)
⊢ (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) = fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
ext N
State after:
case h.e'_3.h
β : 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 : ℕ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0

State before:
case h.e'_3.h
β : 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 : ℕ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
induction' N with N ih
State after:
case h.e'_3.h.zero
β : 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 ∈ Icc (-Int.ofNat 0) ↑0, f n = ∑ i ∈ range (0 + 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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0

State before:
case h.e'_3.h.zero
β : 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 ∈ Icc (-Int.ofNat 0) ↑0, f n = ∑ i ∈ range (0 + 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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
. simp
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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0

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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
. have : Icc (- Int.ofNat (Nat.succ N)) (Nat.succ N) = insert (↑(Nat.succ N)) (insert (-Int.ofNat (Nat.succ N)) (Icc (-Int.ofNat N) N)) := by
    rw [←Ico_insert_right, ←Ioo_insert_left]
    . congr
      ext n
      simp only [Int.ofNat_eq_coe, 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_coe, add_right_inj]
  rw [add_comm]
  . simp
  . norm_num
    linarith
State after:
no goals

State before:
case h.e'_3.h.zero
β : 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 ∈ Icc (-Int.ofNat 0) ↑0, f n = ∑ i ∈ range (0 + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
simp
State after:
no goals

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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
have : Icc (- Int.ofNat (Nat.succ N)) (Nat.succ N) = insert (↑(Nat.succ N)) (insert (-Int.ofNat (Nat.succ N)) (Icc (-Int.ofNat N) N)) := by
  rw [←Ico_insert_right, ←Ioo_insert_left]
  . congr
    ext n
    simp only [Int.ofNat_eq_coe, 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
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))
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0

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))
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
rw [this, sum_insert, sum_insert, ih, ←add_assoc]
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.succ + f (-Int.ofNat N.succ) + (∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0) =
    ∑ i ∈ range (N + 1 + 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)

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))
⊢ f ↑N.succ + f (-Int.ofNat N.succ) + (∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0) =
    ∑ i ∈ range (N + 1 + 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:
symm
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))
⊢ ∑ 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)

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]
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)

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))
⊢ 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)
Tactic:
simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,
  Int.ofNat_eq_coe, add_right_inj]
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 0 + ∑ x ∈ range (N + 1), (f ↑x + f (-↑x)) = ∑ x ∈ range (N + 1), (f ↑x + f (-↑x)) + -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)

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))
⊢ -f 0 + ∑ x ∈ range (N + 1), (f ↑x + f (-↑x)) = ∑ x ∈ range (N + 1), (f ↑x + f (-↑x)) + -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 [add_comm]
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))
⊢ -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)

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))
⊢ -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:
. simp
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))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)

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))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)
Tactic:
. norm_num
  linarith
State after:
no goals

State before:
β : 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
⊢ Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
Tactic:
rw [←Ico_insert_right, ←Ioo_insert_left]
State after:
β : 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
⊢ insert (↑N.succ) (insert (-Int.ofNat N.succ) (Ioo (-Int.ofNat N.succ) ↑N.succ)) =
    insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))

β : 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
⊢ -Int.ofNat N.succ < ↑N.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
⊢ -Int.ofNat N.succ ≤ ↑N.succ

State before:
β : 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
⊢ insert (↑N.succ) (insert (-Int.ofNat N.succ) (Ioo (-Int.ofNat N.succ) ↑N.succ)) =
    insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))

β : 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
⊢ -Int.ofNat N.succ < ↑N.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
⊢ -Int.ofNat N.succ ≤ ↑N.succ
Tactic:
. congr
  ext n
  simp only [Int.ofNat_eq_coe, mem_Ioo, mem_Icc]
  push_cast
  rw [Int.lt_add_one_iff, neg_add, ←sub_eq_add_neg, Int.sub_one_lt_iff]
State after:
β : 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
⊢ -Int.ofNat N.succ < ↑N.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
⊢ -Int.ofNat N.succ ≤ ↑N.succ

State before:
β : 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
⊢ -Int.ofNat N.succ < ↑N.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
⊢ -Int.ofNat N.succ ≤ ↑N.succ
Tactic:
. norm_num
  linarith
State after:
β : 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
⊢ -Int.ofNat N.succ ≤ ↑N.succ

State before:
β : 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
⊢ -Int.ofNat N.succ ≤ ↑N.succ
Tactic:
. norm_num
  linarith
State after:
no goals

State before:
β : 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
⊢ insert (↑N.succ) (insert (-Int.ofNat N.succ) (Ioo (-Int.ofNat N.succ) ↑N.succ)) =
    insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
Tactic:
congr
State after:
case e_a.e_a
β : 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
⊢ Ioo (-Int.ofNat N.succ) ↑N.succ = Icc (-Int.ofNat N) ↑N

State before:
case e_a.e_a
β : 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
⊢ Ioo (-Int.ofNat N.succ) ↑N.succ = Icc (-Int.ofNat N) ↑N
Tactic:
ext n
State after:
case e_a.e_a.a
β : 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
n : ℤ
⊢ n ∈ Ioo (-Int.ofNat N.succ) ↑N.succ ↔ n ∈ Icc (-Int.ofNat N) ↑N

State before:
case e_a.e_a.a
β : 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
n : ℤ
⊢ n ∈ Ioo (-Int.ofNat N.succ) ↑N.succ ↔ n ∈ Icc (-Int.ofNat N) ↑N
Tactic:
simp only [Int.ofNat_eq_coe, mem_Ioo, mem_Icc]
State after:
case e_a.e_a.a
β : 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
n : ℤ
⊢ -↑N.succ < n ∧ n < ↑N.succ ↔ -↑N ≤ n ∧ n ≤ ↑N

State before:
case e_a.e_a.a
β : 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
n : ℤ
⊢ -↑N.succ < n ∧ n < ↑N.succ ↔ -↑N ≤ n ∧ n ≤ ↑N
Tactic:
push_cast
State after:
case e_a.e_a.a
β : 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
n : ℤ
⊢ -(↑N + 1) < n ∧ n < ↑N + 1 ↔ -↑N ≤ n ∧ n ≤ ↑N

State before:
case e_a.e_a.a
β : 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
n : ℤ
⊢ -(↑N + 1) < n ∧ n < ↑N + 1 ↔ -↑N ≤ n ∧ n ≤ ↑N
Tactic:
rw [Int.lt_add_one_iff, neg_add, ←sub_eq_add_neg, Int.sub_one_lt_iff]
State after:
no goals

State before:
β : 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
⊢ -Int.ofNat N.succ < ↑N.succ
Tactic:
norm_num
State after:
β : 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
⊢ -1 < ↑N + 1 + ↑N

State before:
β : 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
⊢ -1 < ↑N + 1 + ↑N
Tactic:
linarith
State after:
no goals

State before:
β : 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
⊢ -Int.ofNat N.succ ≤ ↑N.succ
Tactic:
norm_num
State after:
β : 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
⊢ -1 ≤ ↑N + 1 + ↑N

State before:
β : 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
⊢ -1 ≤ ↑N + 1 + ↑N
Tactic:
linarith
State after:
no goals

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))
⊢ -Int.ofNat N.succ ∉ Icc (-Int.ofNat N) ↑N
Tactic:
simp
State after:
no goals

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))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)
Tactic:
norm_num
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))
⊢ ¬↑N + 1 = -1 + -↑N

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))
⊢ ¬↑N + 1 = -1 + -↑N
Tactic:
linarith
State after:
no goals