awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : α
hx : Membership.mem (γ := Set α) {x : α | ClusterPt x f} x
⊢ Membership.mem (γ := Set α) (⋃ y ∈ t, {x : α | (x, y) ∈ id V}) x
have rw : x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)
Tactic: rw [← SetRel.preimage_eq_biUnion, id, ← (hV.2.relPreimage_of_finite htf).closure_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] s)
have rw : TotallyBounded.{u} (α := α) {a : α | ClusterPt a (𝓟 s)}
Tactic: rw [closure_eq_cluster_pts]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ (i : ι), f i) ↔ ∀ (i : ι), (f i).TotallyBounded
have refine : ∀ (h : ∀ (i : ι), (f i).TotallyBounded) (U : SetRel α α) (hU : U ∈ 𝓤 α),
  ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)
Tactic: refine ⟨fun h i ↦ h.mono (le_iSup _ _), fun h U hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)
have choose : ∀ (t : ι → Set α) (htf : ∀ (x : ι), (t x).Finite) (ht : ∀ (x : ι), U.preimage (t x) ∈ f x),
  ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)
Tactic: choose t htf ht using (h · U hU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
⊢ ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)
have refine : Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage (⋃ (i : ι), t i))
Tactic: refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
⊢ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage (⋃ (i : ι), t i))
have simp_rw : ∀ (ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))),
  LE.le.{u} (α := Filter α) (⨆ (i : ι), f i) (⨆ (x : ι), 𝓟 (U.preimage (t x)))
Tactic: simp_rw [U.preimage_iUnion, ← le_principal_iff, ← iSup_principal] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ i ∈ I, f i) ↔ ∀ i ∈ I, (f i).TotallyBounded
have this : Finite.{u_1 + 1} (↑I : Type u_1)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite.{u_1 + 1} (↑I : Type u_1)
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ i ∈ I, f i) ↔ ∀ i ∈ I, (f i).TotallyBounded
have rw : Filter.TotallyBounded.{u} (α := α) (⨆ (x : Subtype (Membership.mem I)), f (↑x : ι)) ↔ ∀ i ∈ I, (f i).TotallyBounded
Tactic: rw [iSup_subtype', totallyBounded_iSup, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite.{u_1 + 1} (↑I : Type u_1)
rw : Filter.TotallyBounded.{u} (α := α) (⨆ (x : Subtype (Membership.mem I)), f (↑x : ι)) ↔ ∀ i ∈ I, (f i).TotallyBounded
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ i ∈ I, f i) ↔ ∀ i ∈ I, (f i).TotallyBounded
have rw₁ : (∀ (i : Subtype (Membership.mem I)), (f (↑i : ι)).TotallyBounded) ↔ ∀ i ∈ I, (f i).TotallyBounded
Tactic: rw [iSup_subtype', totallyBounded_iSup, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite.{u_1 + 1} (↑I : Type u_1)
rw : Filter.TotallyBounded.{u} (α := α) (⨆ (x : Subtype (Membership.mem I)), f (↑x : ι)) ↔ ∀ i ∈ I, (f i).TotallyBounded
rw₁ : (∀ (i : Subtype (Membership.mem I)), (f (↑i : ι)).TotallyBounded) ↔ ∀ i ∈ I, (f i).TotallyBounded
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ i ∈ I, f i) ↔ ∀ i ∈ I, (f i).TotallyBounded
have rw₂ : (∀ (a : ι) (b : a ∈ I), (f (↑(Subtype.mk (p := fun (a : ι) ↦ a ∈ I) a b) : ι)).TotallyBounded) ↔
  ∀ i ∈ I, (f i).TotallyBounded
Tactic: rw [iSup_subtype', totallyBounded_iSup, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
S : Set (Filter α)
hS : S.Finite
⊢ (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded
have rw : Filter.TotallyBounded.{u} (α := α) (⨆ a ∈ S, a) ↔ ∀ f ∈ S, f.TotallyBounded
Tactic: rw [sSup_eq_iSup, totallyBounded_biSup hS]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
S : Set (Filter α)
hS : S.Finite
rw : Filter.TotallyBounded.{u} (α := α) (⨆ a ∈ S, a) ↔ ∀ f ∈ S, f.TotallyBounded
⊢ (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded
have rw₁ : (∀ i ∈ S, i.TotallyBounded) ↔ ∀ f ∈ S, f.TotallyBounded
Tactic: rw [sSup_eq_iSup, totallyBounded_biSup hS]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
s : ι → Set α
⊢ TotallyBounded.{u} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), TotallyBounded (s i)
have simp_rw : Filter.TotallyBounded.{u} (α := α) (𝓟 (⋃ (i : ι), s i)) ↔ ∀ (i : ι), (𝓟 (s i)).TotallyBounded
Tactic: simp_rw [← Filter.totallyBounded_principal_iff, ← Filter.iSup_principal,
    Filter.totallyBounded_iSup]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
s : ι → Set α
simp_rw : Filter.TotallyBounded.{u} (α := α) (𝓟 (⋃ (i : ι), s i)) ↔ ∀ (i : ι), (𝓟 (s i)).TotallyBounded
⊢ TotallyBounded.{u} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), TotallyBounded (s i)
have simp_rw₁ : Filter.TotallyBounded.{u} (α := α) (⨆ (x : ι), 𝓟 (s x)) ↔ ∀ (i : ι), (𝓟 (s i)).TotallyBounded
Tactic: simp_rw [← Filter.totallyBounded_principal_iff, ← Filter.iSup_principal,
    Filter.totallyBounded_iSup]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ TotallyBounded.{u} (α := α) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
have this : Finite.{u_1 + 1} (↑I : Type u_1)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite.{u_1 + 1} (↑I : Type u_1)
⊢ TotallyBounded.{u} (α := α) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
have rw : TotallyBounded.{u} (α := α) (⋃ (x : (↑I : Type u_1)), s (↑x : ι)) ↔ ∀ i ∈ I, TotallyBounded (s i)
Tactic: rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite.{u_1 + 1} (↑I : Type u_1)
rw : TotallyBounded.{u} (α := α) (⋃ (x : (↑I : Type u_1)), s (↑x : ι)) ↔ ∀ i ∈ I, TotallyBounded (s i)
⊢ TotallyBounded.{u} (α := α) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
have rw₁ : (∀ (i : (↑I : Type u_1)), TotallyBounded (s (↑i : ι))) ↔ ∀ i ∈ I, TotallyBounded (s i)
Tactic: rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite.{u_1 + 1} (↑I : Type u_1)
rw : TotallyBounded.{u} (α := α) (⋃ (x : (↑I : Type u_1)), s (↑x : ι)) ↔ ∀ i ∈ I, TotallyBounded (s i)
rw₁ : (∀ (i : (↑I : Type u_1)), TotallyBounded (s (↑i : ι))) ↔ ∀ i ∈ I, TotallyBounded (s i)
⊢ TotallyBounded.{u} (α := α) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
have rw₂ : (∀ (a : ι) (b : a ∈ I), TotallyBounded (s (↑(Subtype.mk (p := fun (a : ι) ↦ a ∈ I) a b) : ι))) ↔
  ∀ i ∈ I, TotallyBounded (s i)
Tactic: rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s
have rw : TotallyBounded.{u} (α := α) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, TotallyBounded s
Tactic: rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
rw : TotallyBounded.{u} (α := α) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, TotallyBounded s
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s
have rw₁ : (∀ i ∈ S, TotallyBounded i) ↔ ∀ s ∈ S, TotallyBounded s
Tactic: rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
⊢ Filter.TotallyBounded.{u} (α := α) ⊥
have rw : TotallyBounded.{u} (α := α) ∅
Tactic: rw [← principal_empty, totallyBounded_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t
have rw : (∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t
Tactic: rw [union_eq_iUnion, totallyBounded_iUnion]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s
have simp_rw : TotallyBounded ({a} ∪ s) ↔ TotallyBounded s
Tactic: simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
simp_rw : TotallyBounded ({a} ∪ s) ↔ TotallyBounded s
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s
have simp_rw₁ : TotallyBounded (α := α) {a} ∧ TotallyBounded s ↔ TotallyBounded s
Tactic: simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
simp_rw : TotallyBounded ({a} ∪ s) ↔ TotallyBounded s
simp_rw₁ : TotallyBounded (α := α) {a} ∧ TotallyBounded s ↔ TotallyBounded s
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s
have simp_rw₂ : True ∧ TotallyBounded s ↔ TotallyBounded s
Tactic: simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
⊢ (f ⊔ g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded
have rw : (∀ (i : Bool), (bif i then f else g).TotallyBounded) ↔ f.TotallyBounded ∧ g.TotallyBounded
Tactic: rw [sup_eq_iSup, totallyBounded_iSup]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
⊢ TotallyBounded (f '' s)
have simp : ∀ (hs : (𝓟 s).TotallyBounded), (map f (𝓟 s)).TotallyBounded
Tactic: simp only [← Filter.totallyBounded_principal_iff, ← Filter.map_principal] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
have mp : g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
mp : g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
⊢ g.TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
have mpr : (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
d : SetRel α α
hd : d ∈ 𝓤 α
⊢ ∃ (t : Set α), t.Finite ∧ d.preimage t ∈ g
have mpr : ∀ (hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g),
  ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c
Tactic: contrapose! H with hd_cover
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
⊢ ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c
have hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
Tactic: have hb : Antitone fun t : Finset α ↦ g ⊓ 𝓟 (d.preimage t)ᶜ :=
      fun s t (h : s ⊆ t) => by beta_reduce; gcongr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
⊢ ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c
have this : f.NeBot
Tactic: have : Filter.NeBot f :=
      (Filter.iInf_neBot_iff_of_directed' <| hb.directed_ge).mpr fun t =>
        Filter.notMem_iff_inf_principal_compl.mp <| hd_cover t t.finite_toSet
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this : f.NeBot
⊢ ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c
have this₁ : f ≤ g
Tactic: have : f ≤ g := iInf_le_of_le ∅ (by simp)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
⊢ ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c
have mpr : ∀ (c : Filter α) (hcf : c ≤ f) (hc : Cauchy c), False
Tactic: refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
⊢ False
have mpr : ∀ (m : Set α) (hm : m ∈ c) (hmd : m ×ˢ m ⊆ d), False
Tactic: rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
⊢ False
have mpr : ∀ (y : α) (hym : y ∈ m), False
Tactic: rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ False
have this₁ : {x : α | (x, y) ∈ d}ᶜ ∈ c
Tactic: have : {x | (x, y) ∈ d}ᶜ ∈ c := by
      simpa [SetRel.preimage] using hcf.trans <| (iInf_le _ {y}).trans inf_le_right
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this_2 : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
this : {x : α | (x, y) ∈ d}ᶜ ∈ c
⊢ False
have mpr : ∀ (z : α) (hzm : z ∈ m) (hyz : Membership.mem (γ := Set α) {x : α | (x, y) ∈ d}ᶜ z), False
Tactic: rcases hc.1.nonempty_of_mem (inter_mem hm this) with ⟨z, hzm, hyz⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)
have refine : ∀ (H : ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)) (f : Filter α),
  f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
Tactic: refine ⟨fun hg f hf => f.cauchy_of_totallyBounded' <| hg.mono hf,
    fun H => g.totallyBounded_iff_filter.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
have rw : (𝓟 s).TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
Tactic: rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_filter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
rw : (𝓟 s).TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
⊢ TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
have rw₁ : (∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c) ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
Tactic: rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_filter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
have rw : (𝓟 s).TotallyBounded ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
Tactic: rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
rw : (𝓟 s).TotallyBounded ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
⊢ TotallyBounded s ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
have rw₁ : (∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)) ↔
  ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
Tactic: rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
⊢ ∃ (x : α), ClusterPt x f
have hmf : (↑m : Filter α) ≤ f
Tactic: have hmf : m ≤ f := Ultrafilter.of_le f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
⊢ ∃ (x : α), ClusterPt x f
have hm : Cauchy (↑m : Filter α)
Tactic: have hm := m.cauchy_of_totallyBounded' (hf.mono hmf)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
hm : Cauchy (↑m : Filter α)
⊢ ∃ (x : α), ClusterPt x f
have obtain : ∀ (x : α) (hx : (↑m : Filter α) ≤ 𝓝 x), ∃ (x : α), ClusterPt x f
Tactic: obtain ⟨x, hx⟩ := CompleteSpace.complete hm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
hm : Cauchy (↑m : Filter α)
x : α
hx : (↑m : Filter α) ≤ 𝓝 x
⊢ ∃ (x : α), ClusterPt x f
have hx₁ : ClusterPt x (↑m : Filter α)
Tactic: rw [le_nhds_iff_adhp_of_cauchy hm] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}
have obtain : ∀ (n : ℕ) (hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a), ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}
Tactic: obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}
have refine : range s ⊆ ⋃ y ∈ s '' {k : ℕ | k ≤ n}, {x : α | (x, y) ∈ a}
Tactic: refine ⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ range s ⊆ ⋃ y ∈ s '' {k : ℕ | k ≤ n}, {x : α | (x, y) ∈ a}
have rw : ∀ (y : ℕ),
  Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} y), {x : α | (x, s y) ∈ a})
    (s y)
Tactic: rw [range_subset_iff, biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} y), {x : α | (x, s y) ∈ a})
    (s m)
have rw : ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i), Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
Tactic: rw [mem_iUnion₂]