awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t

Tactic:
exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem)

Premises used: Iff.mpr, Filter.inter_mem_inf, Filter.forall_mem_nonempty_iff_neBot, mem_nhds_left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
⊢ f ≤ 𝓝 x ↔ ClusterPt x f

Tactic:
⟨fun h => ClusterPt.of_le_nhds' h hf.1, le_nhds_of_cauchy_adhp hf⟩

Premises used: le_nhds_of_cauchy_adhp, ClusterPt.of_le_nhds', And.left, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
hm : UniformContinuous m
⊢ Cauchy (map m f)

Tactic:
⟨hf.1.map _,
    calc
      map m f ×ˢ map m f = map (Prod.map m m) (f ×ˢ f) := Filter.prod_map_map_eq
      _ ≤ Filter.map (Prod.map m m) (𝓤 α) := map_mono hf.right
      _ ≤ 𝓤 β := hm⟩

Premises used: Filter.map_mono, Trans.trans, Cauchy, Filter.NeBot.map, And.right, And.left, And.intro, Filter.prod_map_map_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter β
m : α → β
hf : Cauchy f
hm : Filter.comap (fun (p : α × α) ↦ (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α
inst_1 : (Filter.comap m f).NeBot
⊢ Cauchy (Filter.comap m f)

Tactic:
⟨‹_›,
    calc
      comap m f ×ˢ comap m f = comap (Prod.map m m) (f ×ˢ f) := prod_comap_comap_eq
      _ ≤ comap (Prod.map m m) (𝓤 β) := comap_mono hf.right
      _ ≤ 𝓤 α := hm⟩

Premises used: Trans.trans, Cauchy, Filter.comap_mono, And.right, And.intro, Filter.prod_comap_comap_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter β
m : α → β
hf : Cauchy f
hm : Filter.comap (fun (p : α × α) ↦ (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α
h : (Filter.comap m f).NeBot
⊢ Cauchy (Filter.comap m f)

Tactic:
hf.comap hm

Premises used: Cauchy.comap
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
this : Cauchy (α := { x : α // x ∈ s }) (Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f)
⊢ Cauchy (map m f)

Tactic:
simpa [Set.restrict_def, ← Function.comp_def, ← map_map,
      subtype_coe_map_comap, inf_eq_left.mpr hfs] using this.map hm.restrict

Premises used: Iff.mpr, Set.restrict_def, Cauchy.map, Filter.map_map, UniformContinuousOn.restrict, Function.comp_def, Filter.subtype_coe_map_comap, inf_eq_left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
suffices : Cauchy (α := { x : α // x ∈ s }) (Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f)
⊢ Cauchy (map m f)

Tactic:
suffices Cauchy (comap (Subtype.val : s → α) f) by
    simpa [Set.restrict_def, ← Function.comp_def, ← map_map,
      subtype_coe_map_comap, inf_eq_left.mpr hfs] using this.map hm.restrict
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
⊢ Cauchy (α := { x : α // x ∈ s }) (Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f)

Tactic:
hf.comap' (fun _ x ↦ x) (comap_coe_neBot_of_le_principal (h := hf.1) hfs)

Premises used: Cauchy.comap', Filter.comap_coe_neBot_of_le_principal
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
⊢ Cauchy (α := { x : α // x ∈ s }) (Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f)

Tactic:
exact hf.comap' (fun _ x ↦ x) (comap_coe_neBot_of_le_principal (h := hf.1) hfs)
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
u : β → α
h : CauchySeq u
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right

Premises used: And.right, Filter.Tendsto, Filter.prod_map_map_eq', Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
u : β → α
hu : CauchySeq u
⊢ Nonempty β

Tactic:
@nonempty_of_neBot _ _ <| (map_neBot_iff _).1 hu.1

Premises used: Filter.nonempty_of_neBot
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
⊢ Nonempty β

Tactic:
haveI := h.nonempty
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this : Nonempty β
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
have := h.tendsto_uniformity
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this_1 : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α)

Tactic:
rw [← prod_atTop_atTop_eq] at this

Premises used: Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this_1 : Nonempty β
this : Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α)
⊢ ∃ (k₀ : β), ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
simpa [MapsTo] using atTop_basis.prod_self.tendsto_left_iff.1 this V hV

Premises used: Filter.atTop_basis, Filter.HasBasis.prod_self, Set.MapsTo, Iff.mp, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
f : β → α
x : α
hx : Tendsto f atTop (𝓝 x)
⊢ CauchySeq f

Tactic:
hx.cauchy_map

Premises used: CauchySeq, Filter.Tendsto.cauchy_map
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
x : α
⊢ CauchySeq.{u, v} (α := α) fun (x_1 : β) ↦ x

Tactic:
tendsto_const_nhds.cauchySeq

Premises used: tendsto_const_nhds, Filter.Tendsto.cauchySeq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
⊢ Tendsto (fun (p : β × β) ↦ (u p.1, u p.2)) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α) ↔
    Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simp only [prod_atTop_atTop_eq, Prod.map_def]

Premises used: Filter.prod_atTop_atTop_eq, Prod.map_def
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
inst : Preorder β
inst_1 : SemilatticeSup γ
inst_2 : Nonempty γ
f : β → α
hf : CauchySeq f
g : γ → β
hg : Tendsto g atTop atTop
⊢ CauchySeq (f ∘ g)

Tactic:
⟨inferInstance, le_trans (prod_le_prod.mpr ⟨Tendsto.comp le_rfl hg, Tendsto.comp le_rfl hg⟩) hf.2⟩

Premises used: Iff.mpr, Cauchy, le_rfl, CauchySeq, inferInstance, Filter.prod_le_prod, And.right, And.intro, Filter.Tendsto.comp, le_trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : NoMaxOrder β
inst_2 : Nonempty β
u : ℕ → α
hu : CauchySeq u
f : β → ℕ
hf : Injective f
⊢ CauchySeq (u ∘ f)

Tactic:
hu.comp_tendsto <| Nat.cofinite_eq_atTop ▸ hf.tendsto_cofinite.mono_left atTop_le_cofinite

Premises used: Eq.rec, Function.Injective.tendsto_cofinite, Filter.Tendsto.mono_left, CauchySeq.comp_tendsto, Nat.cofinite_eq_atTop, Filter.atTop_le_cofinite
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u

Tactic:
⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩

Premises used: CauchySeq.comp_injective, Function.Bijective.injective, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
refine : ∀ (H : CauchySeq (u ∘ f)), CauchySeq u
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u

Tactic:
refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ Bijective f

Tactic:
hf
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
lift : ∀ (f : ℕ ≃ ℕ) (H : CauchySeq (β := ℕ) (u ∘ (⇑f : (a : ℕ) → ℕ))), CauchySeq u
⊢ CauchySeq u

Tactic:
lift f to ℕ ≃ ℕ using hf
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (β := ℕ) (u ∘ (⇑f : (a : ℕ) → ℕ))
⊢ CauchySeq u

Tactic:
simpa only [Function.comp_def, f.apply_symm_apply] using H.comp_injective f.symm.injective

Premises used: Equiv.apply_symm_apply, CauchySeq.comp_injective, Function.comp_def, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
rw :
  ∀ (hu : Tendsto (Prod.map u u) atTop (𝓤 α)) {f g : ℕ → ℕ} (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
rw [cauchySeq_iff_tendsto] at hu

Premises used: cauchySeq_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV

Premises used: Set.Mem, Filter.tendsto_atTop_diagonal, Filter.Tendsto.subseq_mem, Prod.map, Filter.Tendsto.prod_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
exact ((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV

Premises used: Filter.tendsto_atTop_diagonal, Filter.Tendsto.subseq_mem, Filter.Tendsto.prod_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
⊢ CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∀ᶠ (k : ℕ × ℕ) in atTop, k ∈ Prod.map u u ⁻¹' V

Tactic:
cauchySeq_iff_tendsto

Premises used: Set.Mem, Filter.Eventually, setOf, Set.Subset, Set.preimage, Filter.Tendsto, cauchySeq_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
⊢ CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod.map_apply]

Premises used: cauchySeq_iff', Prod.map_apply, Set.mem_preimage, Filter.eventually_atTop_prod_self'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
δ : Type u_2
inst : UniformSpace β
inst_1 : Preorder γ
inst_2 : Preorder δ
u : γ → α
v : δ → β
hu : CauchySeq u
hv : CauchySeq v
⊢ CauchySeq (Prod.map u v)

Tactic:
simpa only [CauchySeq, prod_map_map_eq', prod_atTop_atTop_eq] using hu.prod hv

Premises used: CauchySeq, Cauchy.prod, Filter.prod_map_map_eq', Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
inst : UniformSpace β
inst_1 : Preorder γ
u : γ → α
v : γ → β
hu : CauchySeq u
hv : CauchySeq v
⊢ CauchySeq (α := α × β) fun (x : γ) ↦ (u x, v x)

Tactic:
haveI := hu.1.of_map
  (Cauchy.prod hu hv).mono (tendsto_map.prodMk tendsto_map)

Premises used: CauchySeq, Cauchy.mono, Filter.tendsto_map, Cauchy.prod, Filter.Tendsto.prodMk
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
u : β → α
hu : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
⊢ ∀ᶠ (k : β) (l : β) in atTop, (u k, u l) ∈ V

Tactic:
eventually_atTop_curry <| hu.tendsto_uniformity hV

Premises used: Set.Mem, Prod.map, Filter.eventually_atTop_curry, CauchySeq.tendsto_uniformity
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
inst : UniformSpace β
inst_1 : Preorder γ
f : α → β
hf : UniformContinuous f
u : γ → α
hu : CauchySeq u
⊢ CauchySeq (f ∘ u)

Tactic:
hu.map hf

Premises used: CauchySeq, Set.Mem, Filter.map, Cauchy.map, setOf, Set.Subset, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
n : ℕ
rw :
  ∀ (hu : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V) (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
rw [cauchySeq_iff] at hu

Premises used: cauchySeq_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
n : ℕ
rcases : ∀ (N : ℕ) (H : ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V n), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
rcases hu _ (hV n) with ⟨N, H⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
n N : ℕ
H : ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V n
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩

Premises used: Exists.intro, le_trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
n N : ℕ
H : ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V n
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
⊢ ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
have : ∀ n, ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n := fun n => by
    rw [cauchySeq_iff] at hu
    rcases hu _ (hV n) with ⟨N, H⟩
    exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
obtain :
  ∀ (φ : ℕ → ℕ) (φ_extr : StrictMono φ) (hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

Tactic:
obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ∀ l ≥ φ n, (u l, u <| φ n) ∈ V n⟩ :=
    extraction_forall_of_eventually' this

Premises used: Filter.extraction_forall_of_eventually'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

Tactic:
⟨φ, φ_extr, fun n => hφ _ _ (φ_extr <| Nat.lt_add_one n).le⟩

Premises used: LT.lt.le, Nat.lt_add_one, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

Tactic:
exact ⟨φ, φ_extr, fun n => hφ _ _ (φ_extr <| Nat.lt_add_one n).le⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
rcases :
  ∀ (n : ℕ) (hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩

Premises used: UniformSpace.ball_mem_nhds, Filter.mem_atTop_sets, symm_le_uniformity, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
rcases :
  ∀ (φ : ℕ → ℕ) (φ_mono : StrictMono φ)
    (hφV : ∀ (n_1 : ℕ), ((u ∘ fun (a : ℕ) ↦ a + n) (φ (n_1 + 1)), (u ∘ fun (a : ℕ) ↦ a + n) (φ n_1)) ∈ V (n_1 + 1)),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
rcases (hu.comp (tendsto_add_atTop_nat n)).cauchySeq.subseq_mem fun n => hV (n + 1) with
    ⟨φ, φ_mono, hφV⟩

Premises used: Filter.Tendsto.cauchySeq, CauchySeq.subseq_mem, HAdd.hAdd, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφV : ∀ (n_1 : ℕ), ((u ∘ fun (a : ℕ) ↦ a + n) (φ (n_1 + 1)), (u ∘ fun (a : ℕ) ↦ a + n) (φ n_1)) ∈ V (n_1 + 1)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro, StrictMono.add_const, le_add_self
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφV : ∀ (n_1 : ℕ), ((u ∘ fun (a : ℕ) ↦ a + n) (φ (n_1 + 1)), (u ∘ fun (a : ℕ) ↦ a + n) (φ n_1)) ∈ V (n_1 + 1)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
exact ⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
u : β → α
hu : CauchySeq u
ι : Type u_1
f : ι → β
p : Filter ι
inst_1 : p.NeBot
hf : Tendsto f p atTop
a : α
ha : Tendsto (u ∘ f) p (𝓝 a)
⊢ Tendsto u atTop (𝓝 a)

Tactic:
le_nhds_of_cauchy_adhp hu (ha.mapClusterPt.of_comp hf)

Premises used: Filter.Tendsto.mapClusterPt, le_nhds_of_cauchy_adhp, Filter.Tendsto, MapClusterPt.of_comp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
mp : (CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)) → CauchySeq u
mpr : CauchySeq u → CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)
⊢ (CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)) ↔ CauchySeq u

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)
mp :
  ∀ (h : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V),
    ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
⊢ CauchySeq u

Tactic:
rw [cauchySeq_iff] at h ⊢

Premises used: cauchySeq_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
mp : ∀ (N : ℕ) (h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
obtain ⟨N, h⟩ := h V mV
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h_1 : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
h₁ : ∀ k_1 ≥ N + k, ∀ l ≥ N + k, (u k_1, u l) ∈ V
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
use N + k
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h_1 : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ (u (a - k + k), u (b - k + k)) ∈ V

Tactic:
h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb)

Premises used: HSub.hSub, Nat.le_sub_of_add_le
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h_1 : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
h₁ : a = a - k + k
h₂ : b = b - k + k
⊢ (u a, u b) ∈ V

Tactic:
convert! h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb)

Premises used: HSub.hSub, Nat.le_sub_of_add_le
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h_1 : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ a = a - k + k

Tactic:
lia
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h_1 : ∀ V ∈ 𝓤 α, ∃ (N : ℕ), ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ b = b - k + k

Tactic:
lia
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)

Tactic:
h.comp_tendsto (tendsto_add_atTop_nat k)

Premises used: Filter.tendsto_add_atTop_nat, CauchySeq.comp_tendsto