-- Mathlib/Analysis/Normed/Group/Completeness.lean
/-- A normed additive group is complete if any absolutely convergent series converges in the
space. -/
lemma NormedAddCommGroup.completeSpace_of_summable_imp_tendsto
    (h : ∀ u : ℕ → E,
      Summable (‖u ·‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)) :
    CompleteSpace E

Proof state:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))

Tactic:
rw [hv_sum] at ha

Result:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => u (f n) - u (f 0)) atTop (𝓝 a)
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
⊢ (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)

Tactic:
ext n

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
n : ℕ
⊢ ∑ i ∈ range n, v i = u (f n) - u (f 0)

Proof state:
case a
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_summable_dist_of_cauchySeq u hu

Result:
case a.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => dist (u (f (i + 1))) (u (f i))
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
case a.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨a, ha⟩ := h v hf₂

Result:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
case a.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
let v n := u (f (n+1)) - u (f n)

Result:
case a.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
case a.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => dist (u (f (i + 1))) (u (f i))
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
simp only [dist_eq_norm] at hf₂

Result:
case a.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
refine ⟨a + u (f 0), ?_⟩

Result:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ Tendsto u atTop (𝓝 (a + u (f 0)))

Proof state:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => u (f n) - u (f 0)) atTop (𝓝 a)
h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0)))
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))

Tactic:
simpa only [sub_add_cancel] using h₁

Result:
no goals

Proof state:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => u (f n) - u (f 0)) atTop (𝓝 a)
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))

Tactic:
have h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0))) :=
  Tendsto.add_const _ ha

Result:
case a.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n => u (f (n + 1)) - u (f n)
hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)
a : E
ha : Tendsto (fun n => u (f n) - u (f 0)) atTop (𝓝 a)
h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0)))
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))