Theorem: sum_drop (Ray/Analytic/Series.lean)

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
⊢ HasSum (fun n => f (n + 1)) (g - f 0)
Tactic:
have c := sum_cons (a := -f 0) h
State after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ HasSum (fun n => f (n + 1)) (g - f 0)

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ HasSum (fun n => f (n + 1)) (g - f 0)
Tactic:
rw [HasSum]
State after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
rw [neg_add_eq_sub, HasSum, ← tendsto_comp_push, ← tendsto_comp_push] at c
State after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
have s : ((fun N : Finset ℕ ↦ N.sum fun n ↦ (Stream'.cons (-f 0) f) n) ∘ push) ∘ push =
    fun N : Finset ℕ ↦ N.sum fun n ↦ f (n + 1) := by
  clear c h g; apply funext; intro N; simp
  nth_rw 2 [← Stream'.eta f]
  simp only [←push_sum, Stream'.head, Stream'.tail, Stream'.get]
  abel
State after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
rw [s] at c
State after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (fun N => N.sum fun n => f (n + 1)) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (fun N => N.sum fun n => f (n + 1)) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
assumption
State after:
no goals

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
⊢ ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
Tactic:
clear c h g
State after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)

State before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
Tactic:
apply funext
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ∀ (x : Finset ℕ), (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) x = x.sum fun n => f (n + 1)

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ∀ (x : Finset ℕ), (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) x = x.sum fun n => f (n + 1)
Tactic:
intro N
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) N = N.sum fun n => f (n + 1)

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) N = N.sum fun n => f (n + 1)
Tactic:
simp
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) f n) = N.sum fun n => f (n + 1)

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) f n) = N.sum fun n => f (n + 1)
Tactic:
nth_rw 2 [← Stream'.eta f]
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.sum fun n => f (n + 1)

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.sum fun n => f (n + 1)
Tactic:
simp only [←push_sum, Stream'.head, Stream'.tail, Stream'.get]
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ -f 0 + (f 0 + N.sum fun x => f (x + 1)) = N.sum fun x => f (x + 1)

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ -f 0 + (f 0 + N.sum fun x => f (x + 1)) = N.sum fun x => f (x + 1)
Tactic:
abel
State after:
no goals