internlm/Lean-Github huggingface dataset:
Theorem: int_sum_nat
Proof 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
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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0
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
⊢ ∑ 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
Proof state after:
no goals
Theorem: int_sum_nat
Proof 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
Proof state after:
no goals
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
⊢ ∑ 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
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))
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0
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))
⊢ ∑ 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]
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.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)
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))
⊢ -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]
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))
⊢ -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)
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))
⊢ -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
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))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)
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))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)
Tactic:
. norm_num
  linarith
Proof state after:
no goals
Theorem: int_sum_nat
Proof 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]
Proof 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
Theorem: int_sum_nat
Proof 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]
Proof 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
Theorem: int_sum_nat
Proof 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
Proof 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
Theorem: int_sum_nat
Proof 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
Proof state after:
no goals
Theorem: int_sum_nat
Proof 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
Proof 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
Theorem: int_sum_nat
Proof 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
Proof 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
Theorem: int_sum_nat
Proof 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]
Proof 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
Theorem: int_sum_nat
Proof 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
Proof 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
Theorem: int_sum_nat
Proof 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]
Proof state after:
no goals
Theorem: int_sum_nat
Proof 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
Proof 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