awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ V}
⊢ (↑K : Set α) ⊆ V.preimage t

Tactic:
rw [← SetRel.preimage_eq_biUnion] at ht₂

Premises used: SetRel.preimage_eq_biUnion
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l

Tactic:
⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩

Premises used: Filter.mem_lift', And.intro, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
refine :
  ⋃ (K_1 : Compacts α),
      ⋃ (_ :
        Membership.mem (γ := Set (Compacts α))
          {x : Compacts α |
            (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
          K_1),
        (↑K_1 : Set α) ⊆
    U.preimage t
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l

Tactic:
refine ⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
rw :
  ∀ (i : Compacts α)
    (j :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α |
          (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
        i),
    (↑i : Set α) ⊆ U.preimage t
⊢ ⋃ (K_1 : Compacts α),
      ⋃ (_ :
        Membership.mem (γ := Set (Compacts α))
          {x : Compacts α |
            (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
          K_1),
        (↑K_1 : Set α) ⊆
    U.preimage t

Tactic:
rw [Set.iUnion₂_subset_iff]

Premises used: Set.iUnion₂_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
K' : Compacts α
this :
  ((↑K : Set α), (↑K' : Set α)).1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) ((↑K : Set α), (↑K' : Set α)).2 →
    ∀ (hK' : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)), (↑K' : Set α) ⊆ U.preimage t
⊢ ∀
    (j :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α |
          (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
        K'),
    (↑K' : Set α) ⊆ U.preimage t

Tactic:
⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
K' : Compacts α
left_1 : ((↑K : Set α), (↑K' : Set α)).1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) ((↑K : Set α), (↑K' : Set α)).2
hK' : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)
grw : (↑K' : Set α) ⊆ (V.comp V).preimage t
grw₁ : (↑K' : Set α) ⊆ V.preimage (V.preimage t)
grw₂ : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)
grw₃ grw₄ : V.preimage (↑K : Set α) ⊆ V.preimage (↑K : Set α)
⊢ (↑K' : Set α) ⊆ U.preimage t

Tactic:
grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']

Premises used: SetRel.preimage_comp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
⊢ l.TotallyBounded

Tactic:
have hl : l.TotallyBounded := by
    intro U hU
    obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
    obtain ⟨K, hK⟩ := hf (symm_le_uniformity hV) |>.exists
    obtain ⟨t, ht₁, ht₂⟩ := K.isCompact.totallyBounded V hV
    rw [← SetRel.preimage_eq_biUnion] at ht₂
    refine ⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩
    rw [Set.iUnion₂_subset_iff]
    intro K' ⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩
    grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
exists : f ≤ 𝓝 L
⊢ ∃ (x : Compacts α), f ≤ 𝓝 x

Tactic:
exists L
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
simp_rw : f ≤ Filter.comap (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L)) (𝓤 (Compacts α))
⊢ f ≤ 𝓝 L

Tactic:
simp_rw [nhds_eq_comap_uniformity']

Premises used: nhds_eq_comap_uniformity'
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
rw :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] i' →
      Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
          (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i')) ∈
        f
⊢ f ≤ Filter.comap (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L)) (𝓤 (Compacts α))

Tactic:
rw [uniformity_hasBasis_closed.uniformity_compacts.comap _ |>.ge_iff]

Premises used: uniformity_hasBasis_closed, Filter.HasBasis.uniformity_compacts, Filter.HasBasis.ge_iff, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
this :
  ∀ (hU₁ : U ∈ 𝓤 α) (hU₂ : IsClosed[instTopologicalSpaceProd] U),
    Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
        (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)) ∈
      f
⊢ U ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] U →
    Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
        (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)) ∈
      f

Tactic:
⟨hU₁, hU₂⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h_1 : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
h :
  ∀ (K : Compacts α) (hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U),
    Membership.mem (γ := Set (Compacts α))
      (Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
        (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)))
      K
⊢ Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
      (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)) ∈
    f

Tactic:
filter_upwards [hf hU₁] with K hK
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h_1 : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
h : (↑K : Set α) ⊆ U.preimage (↑L : Set α) ∧ (↑L : Set α) ⊆ U.image (↑K : Set α)
⊢ Membership.mem (γ := Set (Compacts α))
    (Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
      (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)))
    K

Tactic:
simp_rw [Set.mem_preimage, Prod.map, id, mem_hausdorffEntourage]

Premises used: id, Prod.map, mem_hausdorffEntourage, Set.mem_preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h_1 : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
h : (↑K : Set α) ⊆ U.preimage (↑L : Set α)
h₁ : (↑L : Set α) ⊆ U.image (↑K : Set α)
⊢ (↑K : Set α) ⊆ U.preimage (↑L : Set α) ∧ (↑L : Set α) ⊆ U.image (↑K : Set α)

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
⊢ let lx := l ⊓ 𝓟 (UniformSpace.ball x U);
  lx = l ⊓ 𝓟 (UniformSpace.ball x U)

Tactic:
set lx := l ⊓ 𝓟 (UniformSpace.ball x U) with le_def

Premises used: UniformSpace.ball, Filter.principal
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
⊢ lx.TotallyBounded

Tactic:
have hlx : lx.TotallyBounded := hl.mono inf_le_left
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
rw : ∀ s ∈ f, ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
⊢ lx.NeBot

Tactic:
rw [le_def, Filter.lift'_inf_principal_eq, Filter.lift'_neBot_iff fun _ _ h =>
        Set.inter_subset_inter_left _ <| Set.biUnion_subset_biUnion_left h]

Premises used: Set.inter_subset_inter_left, Filter.lift'_neBot_iff, Filter.lift'_inf_principal_eq
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
s : Set (Compacts α)
hs : s ∈ f
obtain :
  ∀ (K' : Compacts α) (h₂ : K' ∈ s) (h₁ : ((↑K : Set α), (↑K' : Set α)).1 ⊆ U.preimage ((↑K : Set α), (↑K' : Set α)).2),
    ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
⊢ ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty

Tactic:
obtain ⟨K', ⟨h₁, -⟩, h₂⟩ := Filter.nonempty_of_mem <| Filter.inter_mem hK hs

Premises used: Filter.inter_mem, Filter.nonempty_of_mem
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
s : Set (Compacts α)
hs : s ∈ f
K' : Compacts α
h₂ : K' ∈ s
h₁ : ((↑K : Set α), (↑K' : Set α)).1 ⊆ U.preimage ((↑K : Set α), (↑K' : Set α)).2
obtain :
  ∀ (y : α) (hy : y ∈ ((↑K : Set α), (↑K' : Set α)).2) (hxy : (x, y) ∈ U),
    ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
⊢ ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty

Tactic:
obtain ⟨y, hy, hxy⟩ := h₁ hx
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
s : Set (Compacts α)
hs : s ∈ f
K' : Compacts α
h₂ : K' ∈ s
h₁ : ((↑K : Set α), (↑K' : Set α)).1 ⊆ U.preimage ((↑K : Set α), (↑K' : Set α)).2
y : α
hy : y ∈ ((↑K : Set α), (↑K' : Set α)).2
hxy : (x, y) ∈ U
⊢ ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty

Tactic:
⟨y, Set.mem_iUnion₂_of_mem h₂ hy, hxy⟩

Premises used: Set.mem_iUnion₂_of_mem, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
s : Set (Compacts α)
hs : s ∈ f
K' : Compacts α
h₂ : K' ∈ s
h₁ : ((↑K : Set α), (↑K' : Set α)).1 ⊆ U.preimage ((↑K : Set α), (↑K' : Set α)).2
y : α
hy : y ∈ ((↑K : Set α), (↑K' : Set α)).2
hxy : (x, y) ∈ U
⊢ ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty

Tactic:
exact ⟨y, Set.mem_iUnion₂_of_mem h₂ hy, hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
⊢ lx.NeBot

Tactic:
have : lx.NeBot := by
      rw [le_def, Filter.lift'_inf_principal_eq, Filter.lift'_neBot_iff fun _ _ h =>
        Set.inter_subset_inter_left _ <| Set.biUnion_subset_biUnion_left h]
      intro s hs
      obtain ⟨K', ⟨h₁, -⟩, h₂⟩ := Filter.nonempty_of_mem <| Filter.inter_mem hK hs
      obtain ⟨y, hy, hxy⟩ := h₁ hx
      exact ⟨y, Set.mem_iUnion₂_of_mem h₂ hy, hxy⟩