awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
⊢ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α) = univ
have rw : ∀ (x : ℕ → β), x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
Tactic: rw [eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
⊢ x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
have choose : ∀ (u : (n : ℕ) → α) (hu : ∀ (n : ℕ), u n ∈ A (res x n)),
  x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
Tactic: choose u hu using fun n => hnonempty (res x n)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ Antitone.{0, u_2} (β := Set α) fun (n : ℕ) ↦ A (res x n)
have refine : ∀ (n : ℕ), A (res x (n + 1)) ≤ A (res x n)
Tactic: refine antitone_nat_of_succ_le ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (hypothesis)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
have this : Antitone.{0, u_2} (β := Set α) fun (n : ℕ) ↦ A (res x n)
Tactic: have : Antitone fun n : ℕ => A (res x n) := by
      refine antitone_nat_of_succ_le ?_
      intro n
      apply hanti.antitone
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (hypothesis)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
have umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
Tactic: have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n) := by
    have : Antitone fun n : ℕ => A (res x n) := by
      refine antitone_nat_of_succ_le ?_
      intro n
      apply hanti.antitone
    intro n m hnm
    exact this hnm (hu _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ CauchySeq u
have rw : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
Tactic: rw [Metric.cauchySeq_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
have obtain : ∀ (n : ℕ) (hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε), ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
Tactic: obtain ⟨n, hn⟩ := hdiam.dist_lt _ ε_pos x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
have h : ∀ m ≥ n, ∀ n_1 ≥ n, dist (u m) (u n_1) < ε
Tactic: use n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ dist (u m₀) (u m₁) < ε
have h : u m₀ ∈ A (res x n)
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
h : u m₀ ∈ A (res x n)
⊢ dist (u m₀) (u m₁) < ε
have h₁ : u m₁ ∈ A (res x n)
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₀ ∈ A (res x n)
have h : n ≤ m₀
Tactic: apply umem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₁ ∈ A (res x n)
have h : n ≤ m₁
Tactic: apply umem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (hypothesis)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
have this : CauchySeq u
Tactic: have : CauchySeq u := by
    rw [Metric.cauchySeq_iff]
    intro ε ε_pos
    obtain ⟨n, hn⟩ := hdiam.dist_lt _ ε_pos x
    use n
    intro m₀ hm₀ m₁ hm₁
    apply hn <;> apply umem <;> assumption
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
⊢ x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
have obtain : ∀ (y : α) (hy : Tendsto u atTop (𝓝 y)), x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
Tactic: obtain ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ x ∈ (inducedMap A).fst (β := fun (s : Set (ℕ → β)) ↦ (↑s : Type u_1) → α)
have h : Membership.mem (γ := Set α) (⋂ (n : ℕ), A (res x n)) y
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ Membership.mem (γ := Set α) (⋂ (n : ℕ), A (res x n)) y
have h : ∀ (i : ℕ), y ∈ A (res x i)
Tactic: rw [mem_iInter]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ A (res x n)
have h : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (A (x n :: res x n))
Tactic: apply hanti _ (x n)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (A (x n :: res x n))
have h : ∀ᶠ (x_1 : ℕ) in atTop, u x_1 ∈ A (x n :: res x n)
Tactic: apply mem_closure_of_tendsto hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CantorScheme (goal)
Goal:
β : Type u_1
α : Type u_2
A : List β → Set α
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : (n : ℕ) → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∀ᶠ (x_1 : ℕ) in atTop, u x_1 ∈ A (x n :: res x n)
have h : ∃ (a : ℕ), ∀ b ≥ a, u b ∈ A (x n :: res x n)
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedRing β
hn : IsAbsoluteValue.{0, v} (R := β) norm
f : CauSeq β norm
inst_1 : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
⊢ Membership.mem (γ := Filter ℕ) atTop ((↑f : ℕ → β) ⁻¹' s)
have suffices : ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
Tactic: suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedRing β
hn : IsAbsoluteValue.{0, v} (R := β) norm
f : CauSeq β norm
inst_1 : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
have rcases : ∀ (ε : ℝ) (hε : ε > 0) (hεs : Metric.ball f.lim ε ⊆ s), ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
Tactic: rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedRing β
hn : IsAbsoluteValue.{0, v} (R := β) norm
f : CauSeq β norm
inst_1 : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball f.lim ε ⊆ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
have obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → β) j‖ < ε), ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
Tactic: obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedRing β
hn : IsAbsoluteValue.{0, v} (R := β) norm
f : CauSeq β norm
inst_1 : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball f.lim ε ⊆ s
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → β) j‖ < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
have exists : ∀ b ≥ N, (↑f : ℕ → β) b ∈ s
Tactic: exists N
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedRing β
hn : IsAbsoluteValue.{0, v} (R := β) norm
f : CauSeq β norm
inst_1 : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball f.lim ε ⊆ s
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → β) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ (↑f : ℕ → β) b ∈ s
have a : (↑f : ℕ → β) b ∈ Metric.ball f.lim ε
Tactic: apply hεs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedRing β
hn : IsAbsoluteValue.{0, v} (R := β) norm
f : CauSeq β norm
inst_1 : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball f.lim ε ⊆ s
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → β) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ dist ((↑f : ℕ → β) b) f.lim < ε
have a : ‖f.lim - (↑f : ℕ → β) b‖ < ε
Tactic: rw [dist_comm, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (hypothesis)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
⊢ IsCauSeq norm f
have hf1 : (map f atTop).NeBot
Tactic: obtain ⟨hf1, hf2⟩ := cauchy_iff.1 hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (hypothesis)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
⊢ IsCauSeq norm f
have hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
Tactic: obtain ⟨hf1, hf2⟩ := cauchy_iff.1 hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
have rcases : ∀ (t : Set β) (ht : t ∈ map f atTop) (htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}),
  ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
Tactic: rcases hf2 { x | dist x.1 x.2 < ε } (dist_mem_uniformity hε) with ⟨t, ⟨ht, htsub⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (hypothesis)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
ht : t ∈ map f atTop
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
have ht₁ : ∃ (a : ℕ), ∀ b ≥ a, f b ∈ t
Tactic: simp only [mem_map, mem_atTop_sets, mem_preimage] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
ht : ∃ (a : ℕ), ∀ b ≥ a, f b ∈ t
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
have obtain : ∀ (N : ℕ) (hN : ∀ b ≥ N, f b ∈ t), ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
Tactic: obtain ⟨N, hN⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ b ≥ N, f b ∈ t
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
have exists : ∀ j ≥ N, ‖f j - f N‖ < ε
Tactic: exists N
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ b ≥ N, f b ∈ t
j : ℕ
hj : j ≥ N
⊢ ‖f j - f N‖ < ε
have rw : dist (f j) (f N) < ε
Tactic: rw [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ b ≥ N, f b ∈ t
j : ℕ
hj : j ≥ N
⊢ dist (f j) (f N) < ε
have apply : (f j, f N) ∈ t ×ˢ t
Tactic: apply @htsub (f j, f N)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ b ≥ N, f b ∈ t
j : ℕ
hj : j ≥ N
⊢ (f j, f N) ∈ t ×ˢ t
have ha : f j ∈ t
Tactic: apply Set.mk_mem_prod
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ b ≥ N, f b ∈ t
j : ℕ
hj : j ≥ N
ha : f j ∈ t
⊢ (f j, f N) ∈ t ×ˢ t
have hb : f N ∈ t
Tactic: apply Set.mk_mem_prod
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
⊢ CauchySeq (↑f : ℕ → β)
have refine : ∀ (s : Set (β × β)) (hs : s ∈ uniformity β), ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
Tactic: refine cauchy_iff.2 ⟨by infer_instance, fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
have rcases : ∀ (ε : ℝ) (hε : ε > 0) (hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s), ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
Tactic: rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
⊢ ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
have obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε), ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
Tactic: obtain ⟨N, hN⟩ := CauSeq.cauchy₂ f hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
⊢ ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
have exists : (↑f : ℕ → β) '' {n : ℕ | n ≥ N} ∈ map (↑f : ℕ → β) atTop ∧
  ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
Tactic: exists { n | n ≥ N }.image f
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
⊢ (↑f : ℕ → β) '' {n : ℕ | n ≥ N} ∈ map (↑f : ℕ → β) atTop ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
have simp : (∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ∧
  ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
Tactic: simp only [mem_atTop_sets, mem_map]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
⊢ (∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
have left : ∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
left : ∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}
⊢ (∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
have right : ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}
have left : ∀ b ≥ N, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}
Tactic: exists N
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
b : ℕ
hb : b ≥ N
⊢ b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}
have left : Membership.mem (γ := Set ℕ) {n : ℕ | n ≥ N} b ∧ (↑f : ℕ → β) b = (↑f : ℕ → β) b
Tactic: exists b
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : (↑f : ℕ → β) a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : (↑f : ℕ → β) b' = b
⊢ (a, b) ∈ s
have right : ((↑f : ℕ → β) a', (↑f : ℕ → β) b') ∈ s
Tactic: rw [← ha'2, ← hb'2]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : (↑f : ℕ → β) a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : (↑f : ℕ → β) b' = b
⊢ ((↑f : ℕ → β) a', (↑f : ℕ → β) b') ∈ s
have right : dist ((↑f : ℕ → β) a') ((↑f : ℕ → β) b') < ε
Tactic: apply hεs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CauSeqFilter (goal)
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : (↑f : ℕ → β) a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : (↑f : ℕ → β) b' = b
⊢ dist ((↑f : ℕ → β) a') ((↑f : ℕ → β) b') < ε
have right : ‖(↑f : ℕ → β) a' - (↑f : ℕ → β) b'‖ < ε
Tactic: rw [dist_eq_norm]