awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
rw : (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
rw₁ : l.NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
have rw₂ : l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔
  l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
Tactic: rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
rw : (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
rw₁ : l.NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
rw₂ :
  l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔
    l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
have rw₃ : l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔
  l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α
Tactic: rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
u v : UniformSpace β
F : Filter β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
have rw : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ⊓ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
Tactic: rw [inf_uniformity (u := u), le_inf_iff, and_and_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
u v : UniformSpace β
F : Filter β
rw : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ⊓ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
have rw₁ : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
Tactic: rw [inf_uniformity (u := u), le_inf_iff, and_and_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
u v : UniformSpace β
F : Filter β
rw : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ⊓ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
rw₁ : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
have rw₂ : (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
Tactic: rw [inf_uniformity (u := u), le_inf_iff, and_and_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
ι : Sort u_1
inst : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
have rw : l.NeBot ∧ l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
Tactic: rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
ι : Sort u_1
inst : Nonempty ι
u : ι → UniformSpace β
l : Filter β
rw : l.NeBot ∧ l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
have rw₁ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
Tactic: rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
ι : Sort u_1
inst : Nonempty ι
u : ι → UniformSpace β
l : Filter β
rw : l.NeBot ∧ l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
rw₁ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
have rw₂ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ (∀ (x : ι), l.NeBot) ∧ ∀ (x : ι), l ×ˢ l ≤ 𝓤 β
Tactic: rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
ι : Sort u_1
inst : Nonempty ι
u : ι → UniformSpace β
l : Filter β
rw : l.NeBot ∧ l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
rw₁ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
rw₂ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ (∀ (x : ι), l.NeBot) ∧ ∀ (x : ι), l ×ˢ l ≤ 𝓤 β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
have rw₃ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ l.NeBot ∧ ∀ (x : ι), l ×ˢ l ≤ 𝓤 β
Tactic: rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l
have simp_rw : l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β
Tactic: simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst : l.NeBot
simp_rw : l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l
have simp_rw₁ : l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β
Tactic: simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ Cauchy l ↔ Cauchy (map f l)
have simp : l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)
Tactic: simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
F : Filter (α × β)
simp_rw : Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)
have simp_rw₁ : Cauchy F ↔ Cauchy F ∧ Cauchy F
Tactic: simp_rw +instances [instUniformSpaceProd, ← cauchy_comap_uniformSpace, ← cauchy_inf_uniformSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ Cauchy (f ×ˢ g)
have this : f.NeBot
Tactic: have := hf.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ Cauchy (f ×ˢ g)
have this₁ : g.NeBot
Tactic: have := hg.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f
have rcases : ∀ (U : Set (α × α)) (U_mem : U ∈ 𝓤 α) (hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}), s ∈ f
Tactic: rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}
⊢ s ∈ f
have rcases : ∀ (t : Set α) (t_mem : t ∈ f) (ht : t ×ˢ t ⊆ U) (y : α) (hxy : (x, y) ∈ U) (hy : y ∈ t), s ∈ f
Tactic: rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ s ∈ f
have apply : t ⊆ s
Tactic: apply mem_of_superset t_mem
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
have obtain : ∀ (t : Set α) (t_mem : t ∈ f) (ht : t ×ˢ t ⊆ s), ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
Tactic: obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
have right : ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
Tactic: use t, t_mem, ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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 (map m f)
have suffices : Cauchy (α := { x : α // x ∈ s }) (Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
⊢ ∃ (k₀ : β), ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
have this : Nonempty β
Tactic: haveI := h.nonempty
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this : Nonempty β
⊢ ∃ (k₀ : β), ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
have this₁ : Tendsto (Prod.map u u) atTop (𝓤 α)
Tactic: have := h.tendsto_uniformity
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
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 (𝓤 α)
⊢ ∃ (k₀ : β), ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
have this₁ : Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α)
Tactic: rw [← prod_atTop_atTop_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u
have refine : ∀ (H : CauchySeq (u ∘ f)), CauchySeq u
Tactic: refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ CauchySeq u
have lift : ∀ (f : ℕ ≃ ℕ) (H : CauchySeq (β := ℕ) (u ∘ (⇑f : (a : ℕ) → ℕ))), CauchySeq u
Tactic: lift f to ℕ ≃ ℕ using hf
Cleared hypotheses: f, hf, H
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
have 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
Tactic: rw [cauchySeq_iff_tendsto] at hu
Cleared hypotheses: hu, f, g, hf, hg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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
have 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
Tactic: rw [cauchySeq_iff] at hu
Cleared hypotheses: hu, n
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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 : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
have rcases : ∀ (N : ℕ) (H : ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V n), ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
Tactic: rcases hu _ (hV n) with ⟨N, H⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
have obtain : ∀ (φ : ℕ → ℕ) (φ_extr : StrictMono φ) (hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
have 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)
Tactic: rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
have 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)
Tactic: rcases (hu.comp (tendsto_add_atTop_nat n)).cauchySeq.subseq_mem fun n => hV (n + 1) with
    ⟨φ, φ_mono, hφV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ (CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)) ↔ CauchySeq u
have mp : (CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)) → CauchySeq u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
mp : (CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)) → CauchySeq u
⊢ (CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)) ↔ CauchySeq u
have mpr : CauchySeq u → CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)
⊢ CauchySeq u
have 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
Tactic: rw [cauchySeq_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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 ∈ 𝓤 α
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
have 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
Tactic: obtain ⟨N, h⟩ := h V mV
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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
⊢ ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
have h₁ : ∀ k_1 ≥ N + k, ∀ l ≥ N + k, (u k_1, u l) ∈ V
Tactic: use N + k
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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, u b) ∈ V
have h₁ : a = a - k + k
Tactic: convert! h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
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
⊢ (u a, u b) ∈ V
have h₂ : b = b - k + k
Tactic: convert! h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
have rw : Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α) ↔
  ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Tactic: rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
have refine : (∀ (ib : γ), p ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔
  ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Tactic: refine (atTop_basis.prod_self.tendsto_iff h).trans ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
have refine_1 : ∀ (h : ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i) (i : γ) (hi : p i),
  ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
Tactic: refine H.cauchySeq_iff.trans ⟨fun h i hi => ?_, fun h i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
refine_1 :
  ∀ (h : ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i) (i : γ) (hi : p i),
    ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
have refine_2 : ∀ (h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i) (i : γ) (hi : p i),
  ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Tactic: refine H.cauchySeq_iff.trans ⟨fun h i hi => ?_, fun h i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
have refine_2 : ∀ (t : Set (α × α)) (ht : t ∈ 𝓤 α) (ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) (hts : t ○ t ⊆ s i),
  ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Tactic: rcases comp_symm_of_uniformity (H.mem_of_mem hi) with ⟨t, ht, ht', hts⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
have refine_2 : ∀ (j : γ) (hj : p j) (hjt : s j ⊆ t), ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Tactic: rcases H.mem_iff.1 ht with ⟨j, hj, hjt⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
have refine_2 : ∀ (N : β) (hN : ∀ n ≥ N, (u n, u N) ∈ s j) (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), (u m, u N) ∈ s j
Tactic: refine (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
refine_2 : ∀ (N : β) (hN : ∀ n ≥ N, (u n, u N) ∈ s j) (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), (u m, u N) ∈ s j
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
have refine_2₁ : ∀ (N : β) (hN : ∀ n ≥ N, (u n, u N) ∈ s j) (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), (u n, u N) ∈ s j
Tactic: refine (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.map f f) atTop
have rw : ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
Tactic: rw [mem_map, mem_atTop_sets]