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_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
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
this : lx.NeBot
h : ∀ (y : α) (hy : ClusterPt y lx), x ∈ U.preimage (↑L : Set α)
⊢ x ∈ U.preimage (↑L : Set α)

Tactic:
obtain ⟨y, hy⟩ := hlx.exists_clusterPt

Premises used: Filter.TotallyBounded.exists_clusterPt
-- 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
this : lx.NeBot
y : α
hy : ClusterPt y lx
⊢ ClusterPt y l

Tactic:
have hy₁ : ClusterPt y l := .of_inf_left hy
-- 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
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
⊢ ClusterPt y (𝓟 (UniformSpace.ball x U))

Tactic:
have hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U)) := .of_inf_right hy
-- 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
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U))
⊢ y ∈ UniformSpace.ball x U

Tactic:
rw [← mem_closure_iff_clusterPt, (UniformSpace.isClosed_ball x hU₂).closure_eq] at hy₂

Premises used: IsClosed.closure_eq, mem_closure_iff_clusterPt, UniformSpace.isClosed_ball
-- 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
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : y ∈ UniformSpace.ball x U
⊢ x ∈ U.preimage (↑L : Set α)

Tactic:
⟨y, hy₁, hy₂⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, SetRel.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 : 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
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : y ∈ UniformSpace.ball x U
⊢ x ∈ U.preimage (↑L : Set α)

Tactic:
exact ⟨y, hy₁, hy₂⟩
-- 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
x : α
h : ∀ (hx : ClusterPt x l), x ∈ U.image (↑K : Set α)
⊢ x ∈ (↑L : Set α) → x ∈ U.image (↑K : Set α)

Tactic:
(hx : ClusterPt x 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_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
x : α
hx : ClusterPt x l
h : ClusterPt x (𝓟 (U.image (↑K : Set α)))
⊢ x ∈ U.image (↑K : Set α)

Tactic:
rw [← (hU₂.relImage_of_isCompact K.isCompact).closure_eq, mem_closure_iff_clusterPt]

Premises used: IsClosed.relImage_of_isCompact, IsClosed.closure_eq, mem_closure_iff_clusterPt, TopologicalSpace.Compacts.isCompact
-- 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 : ClusterPt x l
⊢ ClusterPt x (𝓟 (U.image (↑K : Set α)))

Tactic:
hx.mono ?_

Premises used: ClusterPt.mono
-- 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
x : α
hx : ClusterPt x l
h : l ≤ 𝓟 (U.image (↑K : Set α))
⊢ ClusterPt x (𝓟 (U.image (↑K : Set α)))

Tactic:
refine hx.mono ?_

Premises used: ClusterPt.mono
-- 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
x : α
hx : ClusterPt x l
h : U.image (↑K : Set α) ∈ l
⊢ l ≤ 𝓟 (U.image (↑K : Set α))

Tactic:
rw [Filter.le_principal_iff]

Premises used: Filter.le_principal_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 α)
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 : ClusterPt x l
⊢ U.image (↑K : Set α) ∈ l

Tactic:
Filter.mem_of_superset (Filter.mem_lift' hK) ?_

Premises used: Filter.mem_lift', 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_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
x : α
hx : ClusterPt x l
h :
  ⋃ (K_1 : Compacts α),
      ⋃ (_ :
        Membership.mem (γ := Set (Compacts α))
          {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} K_1),
        (↑K_1 : Set α) ⊆
    U.image (↑K : Set α)
⊢ U.image (↑K : Set α) ∈ l

Tactic:
refine Filter.mem_of_superset (Filter.mem_lift' hK) ?_

Premises used: Filter.mem_lift', 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_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
x : α
hx : ClusterPt x l
h :
  ∀ (i : Compacts α)
    (j :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} i),
    (↑i : Set α) ⊆ U.image (↑K : Set α)
⊢ ⋃ (K_1 : Compacts α),
      ⋃ (_ :
        Membership.mem (γ := Set (Compacts α))
          {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} K_1),
        (↑K_1 : Set α) ⊆
    U.image (↑K : Set α)

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 α)
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 : ClusterPt x l
⊢ ∀ (i : Compacts α)
    (j :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} i),
    (↑i : Set α) ⊆ U.image (↑K : Set α)

Tactic:
fun _ ⟨_, h⟩ => h

Premises used: HasSubset.Subset, SetLike.coe, SetRel.image, _private.0.TopologicalSpace.Compacts.instCompleteSpace.match_4
-- 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 : ClusterPt x l
⊢ ∀ (i : Compacts α)
    (j :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} i),
    (↑i : Set α) ⊆ U.image (↑K : Set α)

Tactic:
exact fun _ ⟨_, h⟩ => h
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
K : NonemptyCompacts α
simp_rw :
  Eq (α := Filter (NonemptyCompacts α)) (Filter.comap SetLike.coe (𝓝 (↑K : Set α)))
    (Filter.comap SetLike.coe (𝓝 (↑K : Set α)))
⊢ 𝓝 K = 𝓝 K

Tactic:
simp_rw [nhds_induced, K.isCompact.nhds_hausdorff_eq_nhds_vietoris]

Premises used: nhds_induced, TopologicalSpace.NonemptyCompacts.isCompact, IsCompact.nhds_hausdorff_eq_nhds_vietoris
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Eq (α := Filter (NonemptyCompacts α × NonemptyCompacts α)) (𝓤 (NonemptyCompacts α))
    (Filter.comap (Prod.map SetLike.coe SetLike.coe) ((𝓤 α).lift' hausdorffEntourage))

Tactic:
rfl

Premises used: Set.Mem, uniformity, setOf, Prod.map, rfl, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
ι : Sort u_4
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ Filter.HasBasis.{u_1, u_4} (α := NonemptyCompacts α × NonemptyCompacts α) (𝓤 (NonemptyCompacts α)) p fun (i : ι) ↦
    Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)

Tactic:
h.uniformity_hausdorff.comap _

Premises used: uniformity, setOf, Filter.HasBasis.uniformity_hausdorff, Prod.map, Filter.HasBasis.comap, Filter.comap, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (α := NonemptyCompacts α) SetLike.coe

Tactic:
isUniformEmbedding_coe.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
⊢ UniformContinuous.{u_1, u_1} (α := NonemptyCompacts α) toCloseds

Tactic:
isUniformEmbedding_toCloseds.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
⊢ IsEmbedding.{u_1, u_1} (X := NonemptyCompacts α) toCloseds

Tactic:
isUniformEmbedding_toCloseds.isEmbedding

Premises used: TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
⊢ Continuous.{u_1, u_1} (X := NonemptyCompacts α) toCloseds

Tactic:
uniformContinuous_toCloseds.continuous

Premises used: TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds, UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
inst_2 : CompleteSpace α
⊢ IsClosedEmbedding.{u_1, u_1} (X := NonemptyCompacts α) toCloseds

Tactic:
Compacts.isClosedEmbedding_toCloseds.comp isClosedEmbedding_toCompacts

Premises used: TopologicalSpace.NonemptyCompacts.toCloseds, TopologicalSpace.Compacts.toCloseds, Topology.IsClosedEmbedding.comp, TopologicalSpace.Compacts.isClosedEmbedding_toCloseds, TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous.{u_1, u_1} (α := NonemptyCompacts α) toCompacts

Tactic:
isUniformEmbedding_toCompacts.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ TotallyBounded.{u_1} (α := NonemptyCompacts α) {K : NonemptyCompacts α | (↑K : Set α) ⊆ t}

Tactic:
totallyBounded_preimage isUniformEmbedding_coe.isUniformInducing ht.powerset_hausdorff

Premises used: Set.Mem, setOf, Set.powerset, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, IsUniformEmbedding.isUniformInducing, Set.preimage, TotallyBounded.powerset_hausdorff, totallyBounded_preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsUniformEmbedding (β := NonemptyCompacts α) fun (x : α) ↦ {x}

Tactic:
isUniformEmbedding_coe.of_comp_iff.mp UniformSpace.hausdorff.isUniformEmbedding_singleton

Premises used: UniformSpace.hausdorff.isUniformEmbedding_singleton, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, IsUniformEmbedding.of_comp_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (β := NonemptyCompacts α) fun (x : α) ↦ {x}

Tactic:
isUniformEmbedding_singleton.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_singleton, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → NonemptyCompacts β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous.{u_1, u_2} (β := NonemptyCompacts β) fun (x : α) ↦ f x ⊔ g x

Tactic:
uniformContinuous_sup.comp <| hf.prodMk hg

Premises used: TopologicalSpace.NonemptyCompacts.uniformContinuous_sup, UniformContinuous.prodMk, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (β := NonemptyCompacts (α × β))
    fun (x : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦ x.1 ×ˢ x.2

Tactic:
isUniformEmbedding_coe.uniformContinuous_iff.mpr <|
    UniformSpace.hausdorff.uniformContinuous_prod.comp <|
      uniformContinuous_coe.prodMap uniformContinuous_coe

Premises used: Iff.mpr, UniformContinuous.prodMap, TopologicalSpace.NonemptyCompacts.uniformContinuous_coe, setOf, IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, UniformSpace.hausdorff.uniformContinuous_prod, UniformContinuous.comp, IsUniformInducing.uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → NonemptyCompacts β
g : α → NonemptyCompacts γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous (β := NonemptyCompacts (β × γ)) fun (x : α) ↦ f x ×ˢ g x

Tactic:
uniformContinuous_prod.comp (hf.prodMk hg)

Premises used: UniformContinuous.prodMk, UniformContinuous.comp, TopologicalSpace.NonemptyCompacts.uniformContinuous_prod
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (NonemptyCompacts.map f ⋯)

Tactic:
isUniformEmbedding_coe.uniformContinuous_iff.mpr <| hf.image_hausdorff.comp uniformContinuous_coe

Premises used: Iff.mpr, UniformContinuous.image_hausdorff, TopologicalSpace.NonemptyCompacts.uniformContinuous_coe, IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, UniformContinuous.comp, IsUniformInducing.uniformContinuous_iff