awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this_1 : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left : V.IsSymm
hVU : V.comp V ⊆ U
obtain :
  ∀ (t : Finset α) (ht₁ : ((↑t : Set α), s).1 ⊆ V.preimage ((↑t : Set α), s).2)
    (ht₂ : ((↑t : Set α), s).2 ⊆ V.image ((↑t : Set α), s).1), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
⊢ {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁

Premises used: TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this_1 : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left : V.IsSymm
hVU : V.comp V ⊆ U
t : Finset α
ht₁ : (↑t : Set α) ⊆ V.preimage s
ht₂ : s ⊆ V.image (↑t : Set α)
u : Set α
h : ∀ (hu : (↑t : Set α) ⊆ V.preimage u), s ⊆ U.preimage u
⊢ (∀ i ∈ t, (u ∩ UniformSpace.ball i V).Nonempty) → s ⊆ U.preimage u

Tactic:
(hu : ↑t ⊆ V.preimage ↑u)
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this_1 : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left : V.IsSymm
hVU : V.comp V ⊆ U
t : Finset α
ht₁ : (↑t : Set α) ⊆ V.preimage s
ht₂ : s ⊆ V.image (↑t : Set α)
h : ∀ (u : Set α) (hu : (↑t : Set α) ⊆ V.preimage u), s ⊆ U.preimage u
⊢ {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s

Tactic:
filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this_1 : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left : V.IsSymm
hVU : V.comp V ⊆ U
t : Finset α
ht₁ : (↑t : Set α) ⊆ V.preimage s
ht₂ : s ⊆ V.image (↑t : Set α)
u : Set α
hu : (↑t : Set α) ⊆ V.preimage u
h : V.image (↑t : Set α) ⊆ U.preimage u
h₁ : V.preimage (↑t : Set α) ⊆ U.preimage u
h₂ : V.preimage (V.preimage u) ⊆ U.preimage u
h₃ : V.preimage (V.preimage u) ⊆ (V.comp V).preimage u
h₄ h₅ : V.preimage (V.preimage u) ⊆ V.preimage (V.preimage u)
⊢ s ⊆ U.preimage u

Tactic:
grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]

Premises used: SetRel.preimage_comp, SetRel.preimage_eq_image
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s = 𝓝 s

Tactic:
le_antisymm ?_ hs.totallyBounded.nhds_vietoris_le_nhds_hausdorff

Premises used: IsCompact.totallyBounded, le_antisymm, TotallyBounded.nhds_vietoris_le_nhds_hausdorff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
refine : 𝓝 s ≤ 𝓝 s
⊢ 𝓝 s = 𝓝 s

Tactic:
refine le_antisymm ?_ hs.totallyBounded.nhds_vietoris_le_nhds_hausdorff

Premises used: IsCompact.totallyBounded, le_antisymm, TotallyBounded.nhds_vietoris_le_nhds_hausdorff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
simp_rw :
  ∀ (i : Set (Set α))
    (j :
      Membership.mem (γ := Set (Set (Set α)))
        {s_1 : Set (Set α) |
          s ∈ s_1 ∧
            Membership.mem (γ := Set (Set (Set α)))
              (Set.powerset '' {U : Set α | IsOpen[inst.toTopologicalSpace] U} ∪
                (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst.toTopologicalSpace] U})
              s_1}
        i),
    i ∈ 𝓝 s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
simp_rw [TopologicalSpace.nhds_generateFrom, le_iInf₂_iff, Filter.le_principal_iff]

Premises used: Filter.le_principal_iff, TopologicalSpace.nhds_generateFrom, le_iInf₂_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
inl : ∀ (V : SetRel α α) (hV₁ : V ∈ 𝓤 α) (hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U), 𝒫 U ∈ 𝓝 s
⊢ 𝒫 U ∈ 𝓝 s

Tactic:
obtain ⟨V : SetRel α α, hV₁, hV₂⟩ :=
      hs.nhdsSet_basis_uniformity (𝓤 α).basis_sets |>.mem_iff.mp (hU.mem_nhdsSet.mpr hs')

Premises used: Iff.mpr, Filter.HasBasis.mem_iff, SetRel, uniformity, Filter.basis_sets, Iff.mp, IsCompact.nhdsSet_basis_uniformity, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
t : Set α
h : (s, t).1 ⊆ V.preimage (s, t).2 → ∀ (ht : (s, t).2 ⊆ V.image (s, t).1), t ∈ 𝒫 U
⊢ t ∈ UniformSpace.ball s (hausdorffEntourage V) → t ∈ 𝒫 U

Tactic:
⟨_, ht⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
h : ∀ (t : Set α), (s, t).1 ⊆ V.preimage (s, t).2 → ∀ (ht : (s, t).2 ⊆ V.image (s, t).1), t ∈ 𝒫 U
⊢ 𝒫 U ∈ 𝓝 s

Tactic:
filter_upwards [UniformSpace.ball_mem_nhds _ (Filter.mem_lift' hV₁)]
      with t ⟨_, ht⟩

Premises used: UniformSpace.ball_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
t : Set α
left : (s, t).1 ⊆ V.preimage (s, t).2
ht : (s, t).2 ⊆ V.image (s, t).1
⊢ t ∈ 𝒫 U

Tactic:
ht.trans fun x ⟨y, hy, hxy⟩ => hV₂ <| Set.mem_biUnion hy hxy

Premises used: Set.Mem, setOf, _private.0.IsCompact.nhds_hausdorff_eq_nhds_vietoris.match_3, Set.powerset, Membership.mem, HasSubset.Subset.trans, Set.mem_biUnion
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
t : Set α
left : (s, t).1 ⊆ V.preimage (s, t).2
ht : (s, t).2 ⊆ V.image (s, t).1
⊢ t ∈ 𝒫 U

Tactic:
exact ht.trans fun x ⟨y, hy, hxy⟩ => hV₂ <| Set.mem_biUnion hy hxy

Premises used: _private.0.IsCompact.nhds_hausdorff_eq_nhds_vietoris.match_3, Membership.mem, HasSubset.Subset.trans, Set.mem_biUnion
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U) s
⊢ (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ 𝓝 s

Tactic:
(UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen hU).mem_nhds hs'

Premises used: Set.Mem, UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen, IsOpen.mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U) s
⊢ (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ 𝓝 s

Tactic:
exact (UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen hU).mem_nhds hs'

Premises used: UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen, IsOpen.mem_nhds
-- 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 α
rw :
  ∀ (f : Ultrafilter (Set α)),
    (↑f : Filter (Set α)) ≤ 𝓟 Set.univ →
      ∃ (x : Set α), Membership.mem (γ := Set (Set α)) Set.univ x ∧ (↑f : Filter (Set α)) ≤ 𝓝 x
⊢ IsCompact.{u_1} (X := Set α) Set.univ

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Premises used: isCompact_iff_ultrafilter_le_nhds
-- 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 α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ ∃ (x : Set α), Membership.mem (γ := Set (Set α)) Set.univ x ∧ (↑f : Filter (Set α)) ≤ 𝓝 x

Tactic:
⟨closure f.lim, Set.mem_univ _, ?_⟩

Premises used: closure, And.intro, Exists.intro, Set.mem_univ, Ultrafilter.lim
-- 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 α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
refine : (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
⊢ ∃ (x : Set α), Membership.mem (γ := Set (Set α)) Set.univ x ∧ (↑f : Filter (Set α)) ≤ 𝓝 x

Tactic:
refine ⟨closure f.lim, Set.mem_univ _, ?_⟩
-- 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 α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
grw : (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
grw₁ : (↑f : Filter (Set α)) ≤ 𝓝 f.lim
grw₂ grw₃ : 𝓝 f.lim ≤ 𝓝 f.lim
⊢ (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)

Tactic:
grw [isClosed_closure.isCompact.nhds_hausdorff_eq_nhds_vietoris,
      ← TopologicalSpace.vietoris.specializes_closure.nhds_le_nhds, f.le_nhds_lim]

Premises used: TopologicalSpace.vietoris.specializes_closure, Specializes.nhds_le_nhds, Ultrafilter.le_nhds_lim, IsClosed.isCompact, IsCompact.nhds_hausdorff_eq_nhds_vietoris, isClosed_closure
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Eq (α := Filter (Closeds α × Closeds α)) (𝓤 (Closeds α))
    (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} (α := Closeds α × Closeds α) (𝓤 (Closeds α)) 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 (α := Closeds α) SetLike.coe

Tactic:
isUniformEmbedding_coe.uniformContinuous

Premises used: TopologicalSpace.Closeds.isUniformEmbedding_coe, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsOpen[inst.toTopologicalSpace] s
⊢ IsOpen.{u_1} (X := Closeds α) {t : Closeds α | ((↑t : Set α) ∩ s).Nonempty}

Tactic:
isOpen_induced (UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen hs)

Premises used: Set.Mem, setOf, UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen, isOpen_induced, Set.Nonempty, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsClosed[inst.toTopologicalSpace] s
⊢ IsClosed.{u_1} (X := Closeds α) {t : Closeds α | (↑t : Set α) ⊆ s}

Tactic:
isClosed_induced hs.powerset_hausdorff

Premises used: Set.Mem, setOf, Set.powerset, Set.preimage, IsClosed.powerset_hausdorff, isClosed_induced
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClopen (X := Closeds α) (SetLike.coe ⁻¹' {∅})

Tactic:
UniformSpace.hausdorff.isClopen_singleton_empty.preimage uniformContinuous_coe.continuous

Premises used: UniformSpace.hausdorff.isClopen_singleton_empty, UniformContinuous.continuous, TopologicalSpace.Closeds.uniformContinuous_coe, IsClopen.preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : Eq (α := Set (Closeds α)) {⊥} (SetLike.coe ⁻¹' {∅})
⊢ IsClopen (X := Closeds α) {⊥}

Tactic:
convert! UniformSpace.hausdorff.isClopen_singleton_empty.preimage uniformContinuous_coe.continuous

Premises used: UniformSpace.hausdorff.isClopen_singleton_empty, UniformContinuous.continuous, TopologicalSpace.Closeds.uniformContinuous_coe, IsClopen.preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h :
  ∀ (x : Closeds α),
    Membership.mem (γ := Set (Closeds α)) {⊥} x ↔ Membership.mem (γ := Set (Closeds α)) (SetLike.coe ⁻¹' {∅}) x
⊢ Eq (α := Set (Closeds α)) {⊥} (SetLike.coe ⁻¹' {∅})

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
x : Closeds α
⊢ Membership.mem (γ := Set (Closeds α)) {⊥} x ↔ Membership.mem (γ := Set (Closeds α)) (SetLike.coe ⁻¹' {∅}) x

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ TotallyBounded.{u_1} (α := Closeds α) {F : Closeds α | (↑F : Set α) ⊆ t}

Tactic:
totallyBounded_preimage isUniformEmbedding_coe.isUniformInducing ht.powerset_hausdorff

Premises used: TopologicalSpace.Closeds.isUniformEmbedding_coe, Set.Mem, setOf, Set.powerset, IsUniformEmbedding.isUniformInducing, Set.preimage, TotallyBounded.powerset_hausdorff, totallyBounded_preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClosed.{u_1} (X := Closeds α) {s : Closeds α | TotallyBounded (↑s : Set α)}

Tactic:
UniformSpace.hausdorff.isClosed_setOf_totallyBounded.preimage uniformContinuous_coe.continuous

Premises used: UniformSpace.hausdorff.isClosed_setOf_totallyBounded, TotallyBounded, Set.Mem, setOf, UniformContinuous.continuous, Set.preimage, IsClosed.preimage, TopologicalSpace.Closeds.uniformContinuous_coe
-- 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} (Closeds α)

Tactic:
isUniformEmbedding_coe.discreteUniformity

Premises used: TopologicalSpace.Closeds.isUniformEmbedding_coe, IsUniformEmbedding.discreteUniformity
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsUniformEmbedding (β := Closeds α) fun (x : α) ↦ {x}

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

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

Tactic:
isUniformEmbedding_singleton.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, TopologicalSpace.Closeds.isUniformEmbedding_singleton, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsEmbedding (Y := Closeds α) fun (x : α) ↦ {x}

Tactic:
isUniformEmbedding_singleton.isEmbedding

Premises used: TopologicalSpace.Closeds.isUniformEmbedding_singleton, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ Continuous[inst.toTopologicalSpace, _] fun (x : α) ↦ {x}

Tactic:
isEmbedding_singleton.continuous

Premises used: TopologicalSpace.Closeds.isEmbedding_singleton, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
rw :
  IsClosed (X := Closeds α)
    (SetLike.coe ⁻¹' Set.range (ι := α) (Function.comp (β := Closeds α) SetLike.coe fun (x : α) ↦ {x}))
⊢ IsClosed.{u_1} (X := Closeds α) (Set.range fun (x : α) ↦ {x})

Tactic:
rw [← SetLike.coe_injective.preimage_image (s := Set.range ({·})), ← Set.range_comp]

Premises used: Set.range_comp, SetLike.coe_injective, Function.Injective.preimage_image, Set.range, Singleton.singleton
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsClosed (X := Closeds α)
    (SetLike.coe ⁻¹' Set.range (ι := α) (Function.comp (β := Closeds α) SetLike.coe fun (x : α) ↦ {x}))

Tactic:
UniformSpace.hausdorff.isClosedEmbedding_singleton.isClosed_range.preimage
      uniformContinuous_coe.continuous

Premises used: UniformSpace.hausdorff.isClosedEmbedding_singleton, setOf, UniformContinuous.continuous, Set.singleton, IsClosed.preimage, TopologicalSpace.Closeds.uniformContinuous_coe, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsClosed (X := Closeds α)
    (SetLike.coe ⁻¹' Set.range (ι := α) (Function.comp (β := Closeds α) SetLike.coe fun (x : α) ↦ {x}))

Tactic:
exact UniformSpace.hausdorff.isClosedEmbedding_singleton.isClosed_range.preimage
      uniformContinuous_coe.continuous

Premises used: UniformSpace.hausdorff.isClosedEmbedding_singleton, UniformContinuous.continuous, IsClosed.preimage, TopologicalSpace.Closeds.uniformContinuous_coe, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ DiscreteUniformity.{u_1} (Closeds α) ↔ DiscreteUniformity α

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

Premises used: inferInstance, IsUniformEmbedding.discreteUniformity, Iff.intro, TopologicalSpace.Closeds.isUniformEmbedding_singleton
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (β := Closeds α) fun (x : Closeds α × Closeds α) ↦ 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, TopologicalSpace.Closeds.isUniformEmbedding_coe, IsUniformEmbedding.toIsUniformInducing, UniformContinuous.comp, UniformSpace.hausdorff.uniformContinuous_union, IsUniformInducing.uniformContinuous_iff, TopologicalSpace.Closeds.uniformContinuous_coe
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → Closeds β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous.{u_1, u_2} (β := Closeds β) fun (x : α) ↦ f x ⊔ g x

Tactic:
uniformContinuous_sup.comp <| hf.prodMk hg

Premises used: UniformContinuous.prodMk, UniformContinuous.comp, TopologicalSpace.Closeds.uniformContinuous_sup
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
⊢ ContinuousSup.{u_1} (Closeds α)

Tactic:
⟨uniformContinuous_sup.continuous⟩

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

Tactic:
uniformContinuous_prod.comp (hf.prodMk hg)

Premises used: UniformContinuous.prodMk, UniformContinuous.comp, TopologicalSpace.Closeds.uniformContinuous_prod
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Continuous[_, uniformSpace.toTopologicalSpace] fun (x : Prod.{u_1, u_2} (Closeds α) (Closeds β)) ↦ x.1 ×ˢ x.2

Tactic:
uniformContinuous_prod.continuous

Premises used: setOf, UniformContinuous.continuous, TopologicalSpace.Closeds.uniformContinuous_prod
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
suffices : ∀ (F₁ F₂ : Closeds α), Inseparable F₁ F₂ → F₁ ≤ F₂
⊢ T0Space.{u_1} (Closeds α)

Tactic:
suffices ∀ F₁ F₂ : Closeds α, Inseparable F₁ F₂ → F₁ ≤ F₂ from
    ⟨fun F₁ F₂ h => le_antisymm (this F₁ F₂ h) (this F₂ F₁ h.symm)⟩
-- 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 α), Inseparable F₁ F₂ → F₁ ≤ F₂

Tactic:
fun F₁ F₂ h x hx₁ => isClosed_iff_frequently.mp F₂.isClosed _ ?_

Premises used: TopologicalSpace.Closeds.isClosed, isClosed_iff_frequently, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
refine : ∀ (F₁ F₂ : Closeds α) (h : Inseparable F₁ F₂) (x : α) (hx₁ : x ∈ F₁), ∃ᶠ (y : α) in 𝓝 x, y ∈ (↑F₂ : Set α)
⊢ ∀ (F₁ F₂ : Closeds α), Inseparable F₁ F₂ → F₁ ≤ F₂

Tactic:
refine fun F₁ F₂ h x hx₁ => isClosed_iff_frequently.mp F₂.isClosed _ ?_

Premises used: isClosed_iff_frequently, Iff.mp
-- 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 : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
rw : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)
⊢ ∃ᶠ (y : α) in 𝓝 x, y ∈ (↑F₂ : Set α)

Tactic:
rw [nhds_eq_comap_uniformity, Filter.frequently_comap, Filter.frequently_iff]

Premises used: Filter.frequently_iff, Filter.frequently_comap, 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 γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ (↑F₁ : Set α) ⊆ U.preimage (↑F₂ : Set α)

Tactic:
obtain ⟨h : (F₁ : Set α) ⊆ U.preimage F₂, -⟩ :=
    mem_of_mem_nhds <| h.nhds_le_uniformity <| Filter.preimage_mem_comap <| Filter.mem_lift' hU

Premises used: Filter.mem_lift', mem_of_mem_nhds, SetLike.coe, Filter.preimage_mem_comap, Inseparable.nhds_le_uniformity, SetRel.preimage