awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ 𝓤 α
⊢ ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
have obtain : ∀ (N : β) (hN : U N ⊆ s), ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
Tactic: obtain ⟨N, hN⟩ := hU s hs
-- 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 ∈ 𝓤 α
N : β
hN : U N ⊆ s
⊢ ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
have refine : ∀ (mn : β × β) (hmn : mn ≥ (N, N)), mn ∈ Prod.map f f ⁻¹' s
Tactic: refine ⟨(N, N), fun mn hmn => ?_⟩
-- 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 ∈ 𝓤 α
N : β
hN : U N ⊆ s
mn : β × β
hmn : mn ≥ (N, N)
⊢ mn ∈ Prod.map f f ⁻¹' s
have obtain : ∀ (m n : β) (hmn : (m, n) ≥ (N, N)), (m, n) ∈ Prod.map f f ⁻¹' s
Tactic: obtain ⟨m, n⟩ := mn
Cleared hypotheses: mn, hmn
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
have refine : ∀ (H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x)
  (l : Filter α) (hl : Cauchy l) (hls : l ≤ 𝓟 s), ∃ x ∈ s, ClusterPt x l
Tactic: refine ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x l
have this : l.NeBot
Tactic: haveI := hl.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, ClusterPt x l
have rcases : ∀ (x : α) (hxs : x ∈ s) (hxl : (↑(Ultrafilter.of l) : Filter α) ≤ 𝓝 x), ∃ x ∈ s, ClusterPt x l
Tactic: rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : IsComplete s
ht : IsComplete t
⊢ IsComplete (s ∪ t)
have simp : ∀ (hs : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → s ∈ l → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x)
  (ht : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → t ∈ l → ∃ x ∈ t, (↑l : Filter α) ≤ 𝓝 x) (l : Ultrafilter α),
  Cauchy (↑l : Filter α) → (s ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x)
Tactic: simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 S
⊢ ∃ x ∈ S, l ≤ 𝓝 x
have hls₁ : S ∈ l
Tactic: rw [le_principal_iff] at hls
Cleared hypotheses: hls
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
⊢ ∃ x ∈ S, l ≤ 𝓝 x
have hl_ne : l.NeBot
Tactic: obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
⊢ ∃ x ∈ S, l ≤ 𝓝 x
have hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
Tactic: obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U
have rcases : ∀ (t : Set α) (htl : t ∈ l) (htU : t ×ˢ t ⊆ U), ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U
Tactic: rcases hl' U hU with ⟨t, htl, htU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U
have refine : (t ∩ S) ×ˢ (t ∩ S) ⊆ t ×ˢ t
Tactic: refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ (t ∩ S) ×ˢ (t ∩ S) ⊆ t ×ˢ t
have hs₁ : t ∩ S ⊆ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
⊢ ∃ x ∈ S, l ≤ 𝓝 x
have obtain : ∀ (t : Set α) (htS : t ⊆ S) (htl : t ∈ l) (htU : t ×ˢ t ⊆ U), ∃ x ∈ S, l ≤ 𝓝 x
Tactic: obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ (i : ι), t ⊆ s i
have rcases : ∀ (x : α) (hx : x ∈ t), ∃ (i : ι), t ⊆ s i
Tactic: rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
⊢ ∃ (i : ι), t ⊆ s i
have rcases : ∀ (i : ι) (hi : x ∈ s i), ∃ (i : ι), t ⊆ s i
Tactic: rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
⊢ ∃ (i : ι), t ⊆ s i
have refine : ∀ (y : α) (hy : y ∈ t), y ∈ s i
Tactic: refine ⟨i, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
⊢ y ∈ s i
have rcases : ∀ (j : ι) (hj : y ∈ s j), y ∈ s i
Tactic: rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ x ∈ S, l ≤ 𝓝 x
have obtain : ∀ (i : ι) (hi : t ⊆ s i), ∃ x ∈ S, l ≤ 𝓝 x
Tactic: obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
    rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
    rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
    refine ⟨i, fun y hy => ?_⟩
    rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
    rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
⊢ ∃ x ∈ S, l ≤ 𝓝 x
have rcases : ∀ (x : α) (hxs : x ∈ s i) (hlx : l ≤ 𝓝 x), ∃ x ∈ S, l ≤ 𝓝 x
Tactic: rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
inst : UniformSpace α
inst_1 : CompleteSpace α
f : Filter α
hf : Cauchy f
h : f ≤ 𝓟 univ
⊢ ∃ (x : α), Membership.mem (γ := Set α) univ x ∧ f ≤ 𝓝 x
have rcases : ∀ (x : α) (hx : f ≤ 𝓝 x), ∃ (x : α), Membership.mem (γ := Set α) univ x ∧ f ≤ 𝓝 x
Tactic: rcases CompleteSpace.complete hf with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
⊢ f ≤ 𝓝 (x1, x2)
have rw : Tendsto Prod.fst f (𝓝 x1) ∧ Tendsto Prod.snd f (𝓝 x2)
Tactic: rw [nhds_prod_eq, le_prod]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
⊢ Tendsto Prod.fst f (𝓝 x1) ∧ Tendsto Prod.snd f (𝓝 x2)
have left : Tendsto Prod.fst f (𝓝 x1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
left : Tendsto Prod.fst f (𝓝 x1)
⊢ Tendsto Prod.fst f (𝓝 x1) ∧ Tendsto Prod.snd f (𝓝 x2)
have right : Tendsto Prod.snd f (𝓝 x2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ u '' univ ⊆ K
have rwa : range u ⊆ K
Tactic: rwa [image_univ, range_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ ∃ (x : α), f = pure x
have f_ne_bot : f.NeBot
Tactic: rcases hf with ⟨f_ne_bot, f_le⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
f_ne_bot : f.NeBot
⊢ ∃ (x : α), f = pure x
have f_le : f ×ˢ f ≤ 𝓤 α
Tactic: rcases hf with ⟨f_ne_bot, f_le⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : f ×ˢ f ≤ 𝓤 α
⊢ ∃ (x : α), f = pure x
have f_le₁ : ∃ t₁ ∈ f, ∃ t₂ ∈ f, t₁ ×ˢ t₂ ⊆ SetRel.id
Tactic: simp only [DiscreteUniformity.eq_principal_setRelId, le_principal_iff, mem_prod_iff] at f_le
Cleared hypotheses: f_le
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : ∃ t₁ ∈ f, ∃ t₂ ∈ f, t₁ ×ˢ t₂ ⊆ SetRel.id
⊢ ∃ (x : α), f = pure x
have obtain : ∀ (S : Set α) (hS : S ∈ f) (T : Set α) (hT : T ∈ f) (H : S ×ˢ T ⊆ SetRel.id), ∃ (x : α), f = pure x
Tactic: obtain ⟨S, hS, T, hT, H⟩ := f_le
Cleared hypotheses: f_le
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
S : Set α
hS : S ∈ f
T : Set α
hT : T ∈ f
H : S ×ˢ T ⊆ SetRel.id
⊢ ∃ (x : α), f = pure x
have obtain : ∀ (x : α) (hS hT : {x} ∈ f) (H : SProd.sprod (α := Set α) (β := Set α) {x} {x} ⊆ SetRel.id), ∃ (x : α), f = pure x
Tactic: obtain ⟨x, rfl, _, _, _⟩ := SetRel.exists_eq_singleton_of_prod_subset_id
    (f_ne_bot.nonempty_of_mem hS) (f_ne_bot.nonempty_of_mem hT) H
Cleared hypotheses: S, hS, T, hT, H
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ ∃ (x : α), f ≤ 𝓝 x
have obtain : ∀ (x : α) (hf : Cauchy (pure x)), ∃ (x_1 : α), pure x ≤ 𝓝 x_1
Tactic: obtain ⟨x, rfl⟩ := eq_pure_of_cauchy hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
have rcases : ∀ (r : Set (α × α)) (hr : r ∈ 𝓤 α) (rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r) (rU : r ○ r ⊆ U),
  ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
Tactic: rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
have rcases : ∀ (k : Set α) (fk : k.Finite) (ks : SetRel.preimage r k ∈ f), ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
Tactic: rcases hf r hr with ⟨k, fk, ks⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
have choose : ∀ (g : (x : (↑u : Type u)) → α) (hgs : ∀ (x : (↑u : Type u)), g x ∈ s)
  (hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r), ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
Tactic: choose g hgs hgr using fun x : u => x.coe_prop.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
have refine_1 : range g ⊆ s
Tactic: refine ⟨range g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
refine_1 : range g ⊆ s
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
have refine_2 : (range g).Finite
Tactic: refine ⟨range g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
refine_1 : range g ⊆ s
refine_2 : (range g).Finite
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
have refine_3 : U.preimage (range g) ∈ f
Tactic: refine ⟨range g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
⊢ (range g).Finite
have refine_2 : ∀ (this : Fintype (↑u : Type u)), (range g).Finite
Tactic: haveI : Fintype u := (fk.inter_of_left _).fintype
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
x : α
xs : x ∈ s
⊢ x ∈ SetRel.preimage r k → x ∈ U.preimage (range g)
have h : ∀ (y : α) (hy : y ∈ k) (xy : (x, y) ∈ r), x ∈ U.preimage (range g)
Tactic: ⟨y, hy, xy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
⊢ U.preimage (range g) ∈ f
have h : ∀ (x : α) (xs : x ∈ s) (y : α) (hy : y ∈ k) (xy : (x, y) ∈ r), x ∈ U.preimage (range g)
Tactic: filter_upwards [hs, ks] with x xs ⟨y, hy, xy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
⊢ x ∈ U.preimage (range g)
have h : Membership.mem (γ := Set α) {a : α | ∃ (i : (↑u : Type u)), (a, g i) ∈ U} x
Tactic: simp_rw [SetRel.preimage, exists_range_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
have rw : ∀ (hs : (𝓟 s).TotallyBounded) {U : SetRel α α} (hU : U ∈ 𝓤 α), ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
Tactic: rw [← Filter.totallyBounded_principal_iff] at hs
Cleared hypotheses: hs, U, hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
have simp_rw : ∃ t ⊆ s, t.Finite ∧ s ⊆ U.preimage t
Tactic: simp_rw [← SetRel.preimage_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
⊢ TotallyBounded.{u} (α := α) {x : α | ClusterPt x f}
have refine : ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V),
  ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})
Tactic: refine uniformity_hasBasis_closed.totallyBounded_iff.2 fun V hV => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
⊢ ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})
have obtain : ∀ (t : Set α) (htf : t.Finite) (hst : V.preimage t ∈ f),
  ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})
Tactic: obtain ⟨t, htf, hst⟩ := h V hV.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
⊢ ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | ClusterPt x f} x),
  Membership.mem (γ := Set α) (⋃ y ∈ t, {x : α | (x, y) ∈ id V}) x
Tactic: refine ⟨t, htf, fun x hx => ?_⟩