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 γ
F₁ F₂ : Closeds α
h_1 : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
h : (↑F₁ : Set α) ⊆ U.preimage (↑F₂ : Set α)
obtain : ∀ (y : α) (hy : y ∈ (↑F₂ : Set α)) (hxy : (x, y) ∈ U), ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)
⊢ ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)

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 γ
F₁ F₂ : Closeds α
h_1 : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
h : (↑F₁ : Set α) ⊆ U.preimage (↑F₂ : Set α)
y : α
hy : y ∈ (↑F₂ : Set α)
hxy : (x, y) ∈ U
⊢ ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)

Tactic:
⟨(x, y), hxy, y, rfl, hy⟩

Premises used: Prod.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
F₁ F₂ : Closeds α
h_1 : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
h : (↑F₁ : Set α) ⊆ U.preimage (↑F₂ : Set α)
y : α
hy : y ∈ (↑F₂ : Set α)
hxy : (x, y) ∈ U
⊢ ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)

Tactic:
exact ⟨(x, y), hxy, y, rfl, hy⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsUniformInducing.{u_1, u_1} (α := Set α) (β := Closeds α) Closeds.closure

Tactic:
isUniformEmbedding_coe.isUniformInducing.of_comp_iff.mp
    UniformSpace.hausdorff.isUniformInducing_closure

Premises used: TopologicalSpace.Closeds.isUniformEmbedding_coe, IsUniformInducing.of_comp_iff, IsUniformEmbedding.isUniformInducing, UniformSpace.hausdorff.isUniformInducing_closure, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous.{u_1, u_1} (α := Set α) (β := Closeds α) Closeds.closure

Tactic:
isUniformInducing_closure.uniformContinuous

Premises used: TopologicalSpace.Closeds.isUniformInducing_closure, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Continuous[(UniformSpace.hausdorff α).toTopologicalSpace, _] Closeds.closure

Tactic:
uniformContinuous_closure.continuous

Premises used: TopologicalSpace.Closeds.uniformContinuous_closure, UniformContinuous.continuous
-- 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 : CompactSpace α
⊢ IsCompact.{u_1} (X := Closeds α) Set.univ

Tactic:
simpa [gi.l_surjective.range_eq]
    using isCompact_univ.image continuous_closure

Premises used: TopologicalSpace.Closeds.continuous_closure, Function.Surjective.range_eq, isCompact_univ, GaloisInsertion.l_surjective, IsCompact.image, TopologicalSpace.Closeds.gi
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ CompactSpace.{u_1} (Closeds α) ↔ CompactSpace α

Tactic:
⟨fun _ => compactSpace_of_finite_subfamily_closed fun {ι} F hF₁ hF₂ => ?_,
    fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro, compactSpace_of_finite_subfamily_closed
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
refine :
  CompactSpace.{u_1} (Closeds α) →
    ∀ {ι : Type u_1} (F : ι → Set α) (hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i))
      (hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅), ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
⊢ CompactSpace.{u_1} (Closeds α) ↔ CompactSpace α

Tactic:
refine ⟨fun _ => compactSpace_of_finite_subfamily_closed fun {ι} F hF₁ hF₂ => ?_,
    fun _ => inferInstance⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
⊢ ∀
    (hst :
      Eq (α := Set (Closeds α))
        ({⊥}ᶜ ∩ ⋂ (i : ι), (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅),
    ∃ (u : Finset ι),
      Eq (α := Set (Closeds α))
        ({⊥}ᶜ ∩ ⋂ i ∈ u, (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅

Tactic:
have := isClopen_singleton_bot.compl.isClosed.isCompact.elim_finite_subfamily_closed
    (fun i => {C : Closeds α | ↑C ⊆ F i})
    (fun i => isClosed_subsets_of_isClosed (hF₁ i))
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀
    (hst :
      Eq (α := Set (Closeds α))
        ({⊥}ᶜ ∩ ⋂ (i : ι), (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅),
    ∃ (u : Finset ι),
      Eq (α := Set (Closeds α))
        ({⊥}ᶜ ∩ ⋂ i ∈ u, (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅
⊢ ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}

Tactic:
simp_rw [← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset,
    ← Set.setOf_forall, ← Set.subset_iInter_iff, hF₂, Set.subset_empty_iff, coe_eq_empty,
    Set.setOf_eq_eq_singleton] at this

Premises used: Set.setOf_eq_eq_singleton, Set.disjoint_compl_left_iff_subset, Set.subset_iInter_iff, TopologicalSpace.Closeds.coe_eq_empty, Set.disjoint_iff_inter_eq_empty, Set.subset_empty_iff, Set.setOf_forall
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
obtain :
  ∀ (s : Finset ι) (hs : Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ s, F i} {⊥}),
    ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅

Tactic:
obtain ⟨s, hs⟩ := this .rfl

Premises used: Set.Subset.rfl
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
s : Finset ι
hs : Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ s, F i} {⊥}
⊢ Membership.mem (γ := Set (Closeds α)) {⊥} { carrier := ⋂ i ∈ s, F i, isClosed' := ⋯ }

Tactic:
specialize @hs ⟨⋂ i ∈ s, F i, isClosed_biInter fun i _ => hF₁ i⟩ .rfl

Premises used: Set.Subset.rfl
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
s : Finset ι
hs : Membership.mem (γ := Set (Closeds α)) {⊥} { carrier := ⋂ i ∈ s, F i, isClosed' := ⋯ }
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅

Tactic:
⟨s, congr($hs)⟩

Premises used: congrArg, id, SetLike.coe, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
s : Finset ι
hs : Membership.mem (γ := Set (Closeds α)) {⊥} { carrier := ⋂ i ∈ s, F i, isClosed' := ⋯ }
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅

Tactic:
exact ⟨s, congr($hs)⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
simp_rw : ¬CompactSpace.{u_1} (Closeds α) ↔ ¬CompactSpace α
⊢ NoncompactSpace.{u_1} (Closeds α) ↔ NoncompactSpace α

Tactic:
simp_rw [← not_compactSpace_iff, compactSpace_iff]

Premises used: not_compactSpace_iff, TopologicalSpace.Closeds.compactSpace_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 : NoncompactSpace α
⊢ NoncompactSpace.{u_1} (Closeds α)

Tactic:
noncompactSpace_iff.mpr ‹_›

Premises used: Iff.mpr, TopologicalSpace.Closeds.noncompactSpace_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
K : Compacts α
simp_rw :
  Eq (α := Filter (Compacts α)) (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: TopologicalSpace.Compacts.isCompact, nhds_induced, IsCompact.nhds_hausdorff_eq_nhds_vietoris
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Eq (α := Filter (Compacts α × Compacts α)) (𝓤 (Compacts α))
    (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} (α := Compacts α × Compacts α) (𝓤 (Compacts α)) 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 (α := Compacts α) SetLike.coe

Tactic:
isUniformEmbedding_coe.uniformContinuous

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

Tactic:
isUniformEmbedding_toCloseds.uniformContinuous

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

Tactic:
isUniformEmbedding_toCloseds.isEmbedding

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

Tactic:
uniformContinuous_toCloseds.continuous

Premises used: TopologicalSpace.Compacts.uniformContinuous_toCloseds, UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
inst_2 : CompleteSpace α
⊢ IsClosed.{u_1} (X := Closeds α) {s : Closeds α | TotallyBounded (↑s : Set α)}

Tactic:
Closeds.isClosed_setOf_totallyBounded

Premises used: TopologicalSpace.Closeds.isClosed_setOf_totallyBounded
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
inst_2 : CompleteSpace α
h : Eq.{u_1 + 1} (α := Set (Closeds α)) (Set.range toCloseds) {s : Closeds α | TotallyBounded (↑s : Set α)}
⊢ IsClosed.{u_1} (X := Closeds α) (Set.range toCloseds)

Tactic:
convert! Closeds.isClosed_setOf_totallyBounded

Premises used: TopologicalSpace.Closeds.isClosed_setOf_totallyBounded
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
inst_2 : CompleteSpace α
⊢ Eq.{u_1 + 1} (α := Set (Closeds α)) (Set.range toCloseds) {s : Closeds α | TotallyBounded (↑s : Set α)}

Tactic:
subset_antisymm
      (Set.range_subset_iff.mpr fun K => K.isCompact.totallyBounded)
      (fun K hK => ⟨⟨K, hK.isCompact_of_isClosed K.isClosed⟩, rfl⟩)

Premises used: Iff.mpr, TopologicalSpace.Closeds.isClosed, IsCompact.totallyBounded, subset_antisymm, TopologicalSpace.Compacts.mk, SetLike.coe, TopologicalSpace.Compacts.isCompact, TotallyBounded.isCompact_of_isClosed, Exists.intro, Set.range_subset_iff, rfl
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
inst_2 : CompleteSpace α
⊢ Eq.{u_1 + 1} (α := Set (Closeds α)) (Set.range toCloseds) {s : Closeds α | TotallyBounded (↑s : Set α)}

Tactic:
exact subset_antisymm
      (Set.range_subset_iff.mpr fun K => K.isCompact.totallyBounded)
      (fun K hK => ⟨⟨K, hK.isCompact_of_isClosed K.isClosed⟩, rfl⟩)

Premises used: Iff.mpr, subset_antisymm, Exists.intro, Set.range_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ TotallyBounded.{u_1} (α := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ t}

Tactic:
totallyBounded_preimage isUniformEmbedding_coe.isUniformInducing ht.powerset_hausdorff

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

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

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

Tactic:
isUniformEmbedding_singleton.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.Compacts.isUniformEmbedding_singleton, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (β := Compacts α) fun (x : Compacts α × Compacts α) ↦ x.1 ⊔ x.2

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

Premises used: Iff.mpr, UniformContinuous.prodMap, IsUniformEmbedding.toIsUniformInducing, UniformContinuous.comp, UniformSpace.hausdorff.uniformContinuous_union, TopologicalSpace.Compacts.uniformContinuous_coe, IsUniformInducing.uniformContinuous_iff, TopologicalSpace.Compacts.isUniformEmbedding_coe
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → Compacts β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous.{u_1, u_2} (β := Compacts β) fun (x : α) ↦ f x ⊔ g x

Tactic:
uniformContinuous_sup.comp <| hf.prodMk hg

Premises used: UniformContinuous.prodMk, TopologicalSpace.Compacts.uniformContinuous_sup, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (β := Compacts (α × β)) fun (x : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦ 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, setOf, IsUniformEmbedding.toIsUniformInducing, UniformSpace.hausdorff.uniformContinuous_prod, UniformContinuous.comp, TopologicalSpace.Compacts.uniformContinuous_coe, IsUniformInducing.uniformContinuous_iff, TopologicalSpace.Compacts.isUniformEmbedding_coe
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → Compacts β
g : α → Compacts γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous (β := Compacts (β × γ)) fun (x : α) ↦ f x ×ˢ g x

Tactic:
uniformContinuous_prod.comp (hf.prodMk hg)

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

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

Premises used: Iff.mpr, UniformContinuous.image_hausdorff, IsUniformEmbedding.toIsUniformInducing, UniformContinuous.comp, TopologicalSpace.Compacts.uniformContinuous_coe, IsUniformInducing.uniformContinuous_iff, TopologicalSpace.Compacts.isUniformEmbedding_coe
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ IsUniformInducing (Compacts.map f ⋯)

Tactic:
.of_comp hf.uniformContinuous.compacts_map uniformContinuous_coe <|
    hf.image_hausdorff.comp isUniformEmbedding_coe.isUniformInducing

Premises used: IsUniformEmbedding.isUniformInducing, IsUniformInducing.of_comp, UniformContinuous.compacts_map, TopologicalSpace.Compacts.uniformContinuous_coe, TopologicalSpace.Compacts.isUniformEmbedding_coe, IsUniformInducing.comp, IsUniformInducing.image_hausdorff, IsUniformInducing.uniformContinuous
-- 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 : DiscreteUniformity α
⊢ DiscreteUniformity.{u_1} (Compacts α)

Tactic:
isUniformEmbedding_coe.discreteUniformity

Premises used: IsUniformEmbedding.discreteUniformity, TopologicalSpace.Compacts.isUniformEmbedding_coe
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ DiscreteUniformity.{u_1} (Compacts α) ↔ DiscreteUniformity α

Tactic:
⟨fun _ => isUniformEmbedding_singleton.discreteUniformity, fun _ => inferInstance⟩

Premises used: inferInstance, IsUniformEmbedding.discreteUniformity, TopologicalSpace.Compacts.isUniformEmbedding_singleton, Iff.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 α
⊢ CompleteSpace.{u_1} (Compacts α)

Tactic:
⟨fun {f} ⟨_, hf⟩ => ?_⟩

Premises used: _private.0.TopologicalSpace.Compacts.instCompleteSpace.match_1, Exists, nhds, CompleteSpace.mk, LE.le
-- 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 α
refine : ∀ {f : Filter (Compacts α)}, Cauchy f → f.NeBot → ∀ (hf : f ×ˢ f ≤ 𝓤 (Compacts α)), ∃ (x : Compacts α), f ≤ 𝓝 x
⊢ CompleteSpace.{u_1} (Compacts α)

Tactic:
refine ⟨fun {f} ⟨_, hf⟩ => ?_⟩
-- 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 : f ×ˢ f ≤ 𝓤 (Compacts α)
⊢ ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f

Tactic:
grw [← Filter.curry_le_prod, (𝓤 α).basis_sets.uniformity_compacts.ge_iff] at hf

Premises used: uniformity, Filter.HasBasis.uniformity_compacts, Filter.curry_le_prod, Filter.HasBasis.ge_iff, Filter.basis_sets
-- 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 : ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f
⊢ ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U

Tactic:
change ∀ {U} (hU : U ∈ 𝓤 α), ∀ᶠ K in f, ∀ᶠ K' in f, (↑K, ↑K') ∈ hausdorffEntourage U at hf
-- 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 ∈ 𝓤 α
obtain : ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U), ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l

Tactic:
obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU

Premises used: SetRel, comp_mem_uniformity_sets
-- 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
obtain :
  ∀ (K : Compacts α)
    (hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)),
    ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l

Tactic:
obtain ⟨K, hK⟩ := hf (symm_le_uniformity hV) |>.exists

Premises used: Filter.Eventually.exists, symm_le_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 α)
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)
obtain :
  ∀ (t : Set α) (ht₁ : t.Finite) (ht₂ : (↑K : Set α) ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ V}),
    ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := K.isCompact.totallyBounded V hV

Premises used: IsCompact.totallyBounded, TopologicalSpace.Compacts.isCompact