awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : ∀ s ∈ cocompact F, (⇑f : (a : E) → F) ⁻¹' s ∈ cocompact E
⊢ Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E

Tactic:
specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)

Premises used: Metric.mem_cocompact_of_closedBall_compl_subset, Compl.compl, Eq.subset, Exists.intro, Metric.closedBall, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
rcases :
  ∀ (r : ℝ)
    (hr :
      Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ
        (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)),
    ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
rcases closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩

Premises used: Metric.closedBall_compl_subset_of_mem_cocompact, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
h₁ : ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
use r
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
x : E
hx : r < ‖x‖
this : Membership.mem (γ := Set E) (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ) x
⊢ ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
x : E
hx : r < ‖x‖
h₁ : Membership.mem (γ := Set E) (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ) x
⊢ ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
suffices x ∈ f ⁻¹' (Metric.closedBall 0 ε)ᶜ by simp_all
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
x : E
hx : r < ‖x‖
h₁ : Membership.mem (γ := Set E) (closedBall 0 r)ᶜ x
⊢ Membership.mem (γ := Set E) (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ) x

Tactic:
apply hr
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
x : E
hx : r < ‖x‖
⊢ Membership.mem (γ := Set E) (closedBall 0 r)ᶜ x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
rcases : ∀ (ε : ℝ) (hε : (closedBall 0 ε)ᶜ ⊆ s), f ⁻¹' s ∈ cocompact E
⊢ f ⁻¹' s ∈ cocompact E

Tactic:
rcases closedBall_compl_subset_of_mem_cocompact hs 0 with ⟨ε, hε⟩

Premises used: Metric.closedBall_compl_subset_of_mem_cocompact, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
rcases : ∀ (r : ℝ) (hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖), f ⁻¹' s ∈ cocompact E
⊢ f ⁻¹' s ∈ cocompact E

Tactic:
rcases h ε with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
apply : ∃ (r : ℝ), (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
⊢ f ⁻¹' s ∈ cocompact E

Tactic:
apply mem_cocompact_of_closedBall_compl_subset 0

Premises used: Metric.mem_cocompact_of_closedBall_compl_subset, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
h₁ : (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
⊢ ∃ (r : ℝ), (closedBall 0 r)ᶜ ⊆ f ⁻¹' s

Tactic:
use r
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 r)ᶜ x
⊢ r < ‖x‖

Tactic:
simp only [Set.mem_compl_iff, Metric.mem_closedBall, dist_zero_right, not_le] at hx

Premises used: not_le, Metric.mem_closedBall, dist_zero_right, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
x : E
hx : r < ‖x‖
h₁ : Membership.mem (γ := Set F) (closedBall 0 ε)ᶜ (f x)
⊢ x ∈ f ⁻¹' s

Tactic:
apply hε
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
x : E
hx : r < ‖x‖
⊢ Membership.mem (γ := Set F) (closedBall 0 ε)ᶜ (f x)

Tactic:
simp [hr x hx]
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
n : ℕ
⊢ LT.lt (α := ℝ) 0 ((fun (n : ℕ) ↦ (1 / 2) ^ n) n)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
obtain :
  ∀ (f : ℕ → ℕ) (hf₁ : StrictMono f) (hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n),
    ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_bounded_of_cauchySeq u hu
    (fun n => (1 / (2 : ℝ)) ^ n) (fun n => by positivity)

Premises used: HDiv.hDiv, Metric.exists_subseq_bounded_of_cauchySeq, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))

Tactic:
⟨f, hf₁, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
refine : Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))

Tactic:
refine ⟨f, hf₁, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
n : ℕ
⊢ 0 ≤ dist (u (f (n + 1))) (u (f n))

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
refine : ∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))

Tactic:
refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ summable_geometric_two

Premises used: Summable.of_nonneg_of_le, summable_geometric_two
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b

Tactic:
fun n => le_of_lt <| hf₂ n (f (n + 1)) <| hf₁.monotone (Nat.le_add_right n 1)

Premises used: StrictMono.monotone, Nat.le_add_right, le_of_lt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b

Tactic:
exact fun n => le_of_lt <| hf₂ n (f (n + 1)) <| hf₁.monotone (Nat.le_add_right n 1)

Premises used: StrictMono.monotone, Nat.le_add_right, le_of_lt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
a : ∀ (u : ℕ → E), CauchySeq u → ∃ (a : E), Tendsto u atTop (𝓝 a)
⊢ CompleteSpace E

Tactic:
apply Metric.complete_of_cauchySeq_tendsto

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
a :
  ∀ (f : ℕ → ℕ) (hf₁ : StrictMono f) (hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))),
    ∃ (a : E), Tendsto u atTop (𝓝 a)
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)

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

Premises used: Metric.exists_subseq_summable_dist_of_cauchySeq
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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))
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖

Tactic:
simp only [dist_eq_norm] at hf₂

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
h₁ : ∀ (n : ℕ), ∑ i ∈ range n, v i = u (f n) - u (f 0)
⊢ Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
n : ℕ
⊢ ∑ i ∈ range n, v i = u (f n) - u (f 0)

Tactic:
sum_range_sub (u ∘ f) n

Premises used: Function.comp, Finset.sum_range_sub
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
n : ℕ
⊢ ∑ i ∈ range n, v i = u (f n) - u (f 0)

Tactic:
exact sum_range_sub (u ∘ f) n

Premises used: Function.comp, Finset.sum_range_sub
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
⊢ Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)

Tactic:
have hv_sum : (fun n => (∑ i ∈ range n, v i)) = fun n => u (f n) - u (f 0) := by
    ext n
    exact sum_range_sub (u ∘ f) n
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
a : ∀ (a : E) (ha : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) atTop (𝓝 a)), ∃ (a : E), Tendsto u atTop (𝓝 a)
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨a, ha⟩ := h v hf₂
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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 : E), Tendsto u atTop (𝓝 a)

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

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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 + u (f 0)))
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)

Tactic:
refine ⟨a + u (f 0), ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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)))

Tactic:
tendsto_nhds_of_cauchySeq_of_subseq hu hf₁.tendsto_atTop ?_

Premises used: StrictMono.tendsto_atTop, tendsto_nhds_of_cauchySeq_of_subseq
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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 ∘ f) atTop (𝓝 (a + u (f 0)))
⊢ Tendsto u atTop (𝓝 (a + u (f 0)))

Tactic:
refine tendsto_nhds_of_cauchySeq_of_subseq hu hf₁.tendsto_atTop ?_

Premises used: StrictMono.tendsto_atTop, tendsto_nhds_of_cauchySeq_of_subseq
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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 (fun (n : ℕ) ↦ u (f n) - u (f 0)) atTop (𝓝 a)

Tactic:
rw [hv_sum] at ha
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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 (fun (n : ℕ) ↦ u (f n) - u (f 0) + u (f 0)) 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
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), 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 : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (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₁

Premises used: sub_add_cancel
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
u : ℕ → E
hu : Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖
⊢ ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)

Tactic:
cauchySeq_tendsto_of_complete <| cauchySeq_of_summable_dist ?_

Premises used: cauchySeq_tendsto_of_complete, cauchySeq_of_summable_dist
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
u : ℕ → E
hu : Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖
refine : Summable (α := ℝ) fun (n : ℕ) ↦ dist.{u_1} (α := E) (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)
⊢ ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)

Tactic:
refine cauchySeq_tendsto_of_complete <| cauchySeq_of_summable_dist ?_

Premises used: cauchySeq_tendsto_of_complete, cauchySeq_of_summable_dist
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
u : ℕ → E
hu : Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ dist.{u_1} (α := E) (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)

Tactic:
simp [dist_eq_norm, sum_range_succ, hu]

Premises used: dist_eq_norm, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Normed.Group.Completeness
Goal:
E : Type u_1
inst : NormedAddCommGroup E
⊢ (∀ (u : ℕ → E),
      (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)) ↔
    CompleteSpace E

Tactic:
⟨completeSpace_of_summable_imp_tendsto, fun _ u hu => summable_imp_tendsto_of_complete u hu⟩

Premises used: Iff.intro, NormedAddCommGroup.completeSpace_of_summable_imp_tendsto, NormedAddCommGroup.summable_imp_tendsto_of_complete
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
x : E
⊢ norm (E := Completion E) (↑x : Completion E) = ‖x‖

Tactic:
Completion.extension_coe uniformContinuous_norm x

Premises used: uniformContinuous_norm, UniformSpace.Completion.extension_coe
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
x y : Completion E
hp : IsClosed.{u_1} (X := Completion E × Completion E) {x : Completion E × Completion E | dist x.1 x.2 = ‖-x.1 + x.2‖}
ih :
  ∀ (a b : E),
    dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
      ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
⊢ dist x y = ‖-x + y‖

Tactic:
induction x, y using Completion.induction_on₂
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
⊢ IsClosed.{u_1} (X := Completion E × Completion E) {x : Completion E × Completion E | dist x.1 x.2 = ‖-x.1 + x.2‖}

Tactic:
isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_

Premises used: UniformSpace.Completion.uniformContinuous_extension₂, UniformContinuous.continuous, isClosed_eq