awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.CantorScheme
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 : ℕ
⊢ ∃ (a : ℕ), ∀ b ≥ a, u b ∈ A (x n :: res x n)

Tactic:
exact ⟨n.succ, umem _⟩
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
this : ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
⊢ Membership.mem (γ := Filter ℕ) atTop ((↑f : ℕ → β) ⁻¹' s)

Tactic:
simpa using this
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
suffices : ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
⊢ Membership.mem (γ := Filter ℕ) atTop ((↑f : ℕ → β) ⁻¹' s)

Tactic:
suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
rcases : ∀ (ε : ℝ) (hε : ε > 0) (hεs : Metric.ball f.lim ε ⊆ s), ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s

Tactic:
rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → β) j‖ < ε), ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s

Tactic:
obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ hε

Premises used: CauSeq.equiv_lim, Setoid.symm
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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‖ < ε
exists : ∀ b ≥ N, (↑f : ℕ → β) b ∈ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑f : ℕ → β) b ∈ s

Tactic:
exists N
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
a : (↑f : ℕ → β) b ∈ Metric.ball f.lim ε
⊢ (↑f : ℕ → β) b ∈ s

Tactic:
apply hεs
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
a : ‖f.lim - (↑f : ℕ → β) b‖ < ε
⊢ dist ((↑f : ℕ → β) b) f.lim < ε

Tactic:
rw [dist_comm, dist_eq_norm]

Premises used: dist_eq_norm, dist_comm
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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.lim - (↑f : ℕ → β) b‖ < ε

Tactic:
solve_by_elim
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
⊢ (map f atTop).NeBot

Tactic:
obtain ⟨hf1, hf2⟩ := cauchy_iff.1 hf

Premises used: cauchy_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
⊢ ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s

Tactic:
obtain ⟨hf1, hf2⟩ := cauchy_iff.1 hf

Premises used: cauchy_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
rcases :
  ∀ (t : Set β) (ht : t ∈ map f atTop) (htsub : t ×ˢ t ⊆ {x : β × β | dist x.1 x.2 < ε}),
    ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε

Tactic:
rcases hf2 { x | dist x.1 x.2 < ε } (dist_mem_uniformity hε) with ⟨t, ⟨ht, htsub⟩⟩

Premises used: setOf, Prod.fst, LT.lt, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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 < ε}
⊢ ∃ (a : ℕ), ∀ b ≥ a, f b ∈ t

Tactic:
simp only [mem_map, mem_atTop_sets, mem_preimage] at ht

Premises used: Filter.mem_atTop_sets, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
obtain : ∀ (N : ℕ) (hN : ∀ b ≥ N, f b ∈ t), ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε

Tactic:
obtain ⟨N, hN⟩ := ht
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
exists : ∀ j ≥ N, ‖f j - f N‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖f j - f i‖ < ε

Tactic:
exists N
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
rw : dist (f j) (f N) < ε
⊢ ‖f j - f N‖ < ε

Tactic:
rw [← dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
apply : (f j, f N) ∈ t ×ˢ t
⊢ dist (f j) (f N) < ε

Tactic:
apply @htsub (f j, f N)
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
hb : f N ∈ t
⊢ (f j, f N) ∈ t ×ˢ t

Tactic:
apply Set.mk_mem_prod

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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 ∈ t

Tactic:
solve_by_elim [le_refl]

Premises used: le_refl
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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 N ∈ t

Tactic:
solve_by_elim [le_refl]

Premises used: le_refl
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
⊢ (map (↑f : ℕ → β) atTop).NeBot

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
refine : ∀ (s : Set (β × β)) (hs : s ∈ uniformity β), ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
⊢ CauchySeq (↑f : ℕ → β)

Tactic:
refine cauchy_iff.2 ⟨by infer_instance, fun s hs => ?_⟩

Premises used: Iff.mpr, cauchy_iff, And.intro
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
rcases : ∀ (ε : ℝ) (hε : ε > 0) (hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s), ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
⊢ ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s

Tactic:
rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
obtain :
  ∀ (N : ℕ) (hN : ∀ j ≥ N, ∀ k ≥ N, ‖(↑f : ℕ → β) j - (↑f : ℕ → β) k‖ < ε), ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s
⊢ ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s

Tactic:
obtain ⟨N, hN⟩ := CauSeq.cauchy₂ f hε

Premises used: CauSeq.cauchy₂
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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‖ < ε
exists :
  (↑f : ℕ → β) '' {n : ℕ | n ≥ N} ∈ map (↑f : ℕ → β) atTop ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
⊢ ∃ t ∈ map (↑f : ℕ → β) atTop, t ×ˢ t ⊆ s

Tactic:
exists { n | n ≥ N }.image f

Premises used: setOf, GE.ge, Set.image, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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‖ < ε
simp :
  (∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
⊢ (↑f : ℕ → β) '' {n : ℕ | n ≥ N} ∈ map (↑f : ℕ → β) atTop ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s

Tactic:
simp only [mem_atTop_sets, mem_map]

Premises used: Filter.mem_atTop_sets, Filter.mem_map
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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}
right : ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s
⊢ (∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ∧
    ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ×ˢ ((↑f : ℕ → β) '' {n : ℕ | n ≥ N}) ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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 : ∀ b ≥ N, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}
⊢ ∃ (a : ℕ), ∀ b ≥ a, b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}

Tactic:
exists N
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
left left₁ : Membership.mem (γ := Set ℕ) {n : ℕ | n ≥ N} b ∧ (↑f : ℕ → β) b = (↑f : ℕ → β) b
⊢ b ∈ (↑f : ℕ → β) ⁻¹' (↑f : ℕ → β) '' {n : ℕ | n ≥ N}

Tactic:
exists b
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
right : ((↑f : ℕ → β) a', (↑f : ℕ → β) b') ∈ s
⊢ (a, b) ∈ s

Tactic:
rw [← ha'2, ← hb'2]
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
right : dist ((↑f : ℕ → β) a') ((↑f : ℕ → β) b') < ε
⊢ ((↑f : ℕ → β) a', (↑f : ℕ → β) b') ∈ s

Tactic:
apply hεs
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
right : ‖(↑f : ℕ → β) a' - (↑f : ℕ → β) b'‖ < ε
⊢ dist ((↑f : ℕ → β) a') ((↑f : ℕ → β) b') < ε

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
right : a' ≥ N
right₁ : b' ≥ N
⊢ ‖(↑f : ℕ → β) a' - (↑f : ℕ → β) b'‖ < ε

Tactic:
apply hN
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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' ≥ N

Tactic:
assumption
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
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
⊢ b' ≥ N

Tactic:
assumption
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
α : Type u
inst : NormedField α
u : ℕ → α
⊢ IsCauSeq norm u ↔ CauchySeq u

Tactic:
⟨fun h => CauSeq.cauchySeq ⟨u, h⟩, fun h => h.isCauSeq⟩

Premises used: Subtype.mk, CauSeq.cauchySeq, Iff.intro, CauchySeq.isCauSeq
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
a : ∀ (u : ℕ → β), CauchySeq u → ∃ (a : β), Tendsto u atTop (𝓝 a)
⊢ CompleteSpace β

Tactic:
apply complete_of_cauchySeq_tendsto

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
⊢ IsCauSeq norm u

Tactic:
have C : IsCauSeq norm u := isCauSeq_iff_cauchySeq.2 hu
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
a : Tendsto u atTop (𝓝 (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)))
⊢ ∃ (a : β), Tendsto u atTop (𝓝 a)

Tactic:
exists CauSeq.lim ⟨u, C⟩

Premises used: Subtype.mk, CauSeq.lim
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
a : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)) < ε
⊢ Tendsto u atTop (𝓝 (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)))

Tactic:
rw [Metric.tendsto_atTop]

Premises used: Metric.tendsto_atTop
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
a :
  ∀ (N : ℕ)
    (hN :
      ∀ j ≥ N,
        ‖(↑(Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C -
                    CauSeq.const norm (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C))) :
                ℕ → β)
              j‖ <
          ε),
    ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)) < ε

Tactic:
obtain ⟨N, hN⟩ := (CauSeq.equiv_lim ⟨u, C⟩) _ εpos

Premises used: CauSeq.equiv_lim, Subtype.mk
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN :
  ∀ j ≥ N,
    ‖(↑(Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C -
                CauSeq.const norm (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C))) :
            ℕ → β)
          j‖ <
      ε
a : ∀ n ≥ N, dist (u n) (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)) < ε

Tactic:
exists N
-- Module: Mathlib.Topology.MetricSpace.CauSeqFilter
Goal:
β : Type v
inst : NormedField β
inst_1 : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN :
  ∀ j ≥ N,
    ‖(↑(Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C -
                CauSeq.const norm (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C))) :
            ℕ → β)
          j‖ <
      ε
⊢ ∀ n ≥ N, dist (u n) (CauSeq.lim (Subtype.mk (p := fun (f : ℕ → β) ↦ IsCauSeq norm f) u C)) < ε

Tactic:
simpa [dist_eq_norm] using hN

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
B : ℕ → ℝ
hB : ∀ (n : ℕ), 0 < B n
H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ (x : α), Tendsto u atTop (𝓝 x)
⊢ CompleteSpace α

Tactic:
UniformSpace.complete_of_convergent_controlled_sequences
    (fun n => { p : α × α | dist p.1 p.2 < B n }) (fun n => dist_mem_uniformity <| hB n) H

Premises used: setOf, Prod.fst, LT.lt, UniformSpace.complete_of_convergent_controlled_sequences, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Tendsto u atTop (𝓝 a)) → CompleteSpace α

Tactic:
EMetric.complete_of_cauchySeq_tendsto

Premises used: EMetric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε

Tactic:
uniformity_basis_dist.cauchySeq_iff

Premises used: Filter.HasBasis.cauchySeq_iff, Set.Mem, Metric.uniformity_basis_dist
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, dist (u n) (u N) < ε

Tactic:
uniformity_basis_dist.cauchySeq_iff'

Premises used: Set.Mem, Metric.uniformity_basis_dist, Filter.HasBasis.cauchySeq_iff'
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
mp : UniformCauchySeqOn F atTop s → ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
mpr : (∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε) → UniformCauchySeqOn F atTop s
⊢ UniformCauchySeqOn F atTop s ↔ ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
⊢ ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u

Tactic:
simp [u]
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
⊢ u ∈ 𝓤 α

Tactic:
have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp [u]⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
mp : ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε
⊢ ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
rw [← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]

Premises used: Filter.eventually_atTop_prod_self'
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
specialize h u hu
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
⊢ ∀ᶠ (m : β × β) in atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
rw [prod_atTop_atTop_eq] at h

Premises used: Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε

Tactic:
h.mono fun n h x hx => h x hx

Premises used: Filter.Eventually.mono