awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
a : (Set α × Set α) × Set α × Set α
h :
  ∀ (h₁ : (a.1.1, a.2.1) ∈ hausdorffEntourage U) (h₂ : (a.1.2, a.2.2) ∈ hausdorffEntourage U),
    (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
⊢ a ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
    (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U

Tactic:
⟨h₁, h₂⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
a : (Set α × Set α) × Set α × Set α
h₁ : (a.1.1, a.2.1) ∈ hausdorffEntourage U
h₂ : (a.1.2, a.2.2) ∈ hausdorffEntourage U
⊢ (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U

Tactic:
union_mem_hausdorffEntourage U h₁ h₂

Premises used: union_mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
h :
  ∀ (a : (Set α × Set α) × Set α × Set α),
    Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
      {x : (Set α × Set α) × Set α × Set α |
        x ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
          Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
            {x : (Set α × Set α) × Set α × Set α |
              (fun (a : (Set α × Set α) × Set α × Set α) ↦
                  ((fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.1, (fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.2) ∈
                    hausdorffEntourage U)
                x}
            x}
      a
h₁ :
  ∀ a ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U),
    (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
h₂ :
  ∀ (a : (Set α × Set α) × Set α × Set α) (h₁ : (a.1.1, a.2.1) ∈ hausdorffEntourage U)
    (h₂ : (a.1.2, a.2.2) ∈ hausdorffEntourage U), (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
⊢ ∀ᶠ (a : (Set α × Set α) × Set α × Set α) in 𝓤 (Set α × Set α),
    ((fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.1, (fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.2) ∈ hausdorffEntourage U

Tactic:
filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hU)]
    with _ ⟨h₁, h₂⟩ using union_mem_hausdorffEntourage U h₁ h₂

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

Tactic:
(𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets |>.lift' monotone_hausdorffEntourage
    |>.tendsto_right_iff.mpr fun ⟨U, V⟩ ⟨hU, hV⟩ => ?_

Premises used: Iff.mpr, UniformContinuous, entourageProd, Filter.HasBasis.uniformity_prod, monotone_hausdorffEntourage, iInf, SProd.sprod, Set.Mem, Filter.Eventually, uniformity, _private.0.UniformSpace.hausdorff.uniformContinuous_prod.match_1, Function.comp, Membership.mem, id, Prod.mk, Prod.fst, Filter.basis_sets, Filter.lift', Filter.lift, Filter.HasBasis.tendsto_right_iff, Filter.HasBasis.lift', Prod, _private.0.UniformSpace.hausdorff.uniformContinuous_prod.match_2, Prod.snd, hausdorffEntourage, Set
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
refine :
  ∀ (x : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) (U : Set (α × α)) (V : Set (β × β)),
    (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β →
      ∀ (hU : (U, V).1 ∈ 𝓤 α) (hV : (U, V).2 ∈ 𝓤 β),
        ∀ᶠ (x : Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β)) in
          𝓤 (Prod.{u_1, u_2} (Set α) (Set β)),
          Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
            ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦
                entourageProd (id i.1) (id i.2))
              (U, V))
            ((fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2) x.1,
              (fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2) x.2)
⊢ UniformContinuous (β := Set (α × β)) fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2

Tactic:
refine (𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets |>.lift' monotone_hausdorffEntourage
    |>.tendsto_right_iff.mpr fun ⟨U, V⟩ ⟨hU, hV⟩ => ?_

Premises used: Iff.mpr, entourageProd, Filter.HasBasis.uniformity_prod, monotone_hausdorffEntourage, Filter.Eventually, uniformity, _private.0.UniformSpace.hausdorff.uniformContinuous_prod.match_1, Function.comp, Membership.mem, id, Prod.mk, Prod.fst, Filter.basis_sets, Filter.HasBasis.tendsto_right_iff, Filter.HasBasis.lift', _private.0.UniformSpace.hausdorff.uniformContinuous_prod.match_2, Prod.snd, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
x : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))
U : Set (α × α)
V : Set (β × β)
h_1 : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
s₁ : Set α
s₂ : Set β
t₁ : Set α
t₂ : Set β
h :
  ∀ (h₁ : (s₁, t₁) ∈ hausdorffEntourage U) (h₂ : (s₂, t₂) ∈ hausdorffEntourage V),
    Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
      ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦ entourageProd (id i.1) (id i.2))
        (U, V))
      (((s₁, s₂), t₁, t₂).1.1 ×ˢ ((s₁, s₂), t₁, t₂).1.2, ((s₁, s₂), t₁, t₂).2.1 ×ˢ ((s₁, s₂), t₁, t₂).2.2)
⊢ ((s₁, s₂), t₁, t₂) ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage V) →
    Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
      ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦ entourageProd (id i.1) (id i.2))
        (U, V))
      (((s₁, s₂), t₁, t₂).1.1 ×ˢ ((s₁, s₂), t₁, t₂).1.2, ((s₁, s₂), t₁, t₂).2.1 ×ˢ ((s₁, s₂), t₁, t₂).2.2)

Tactic:
⟨h₁, h₂⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
x : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))
U : Set (α × α)
V : Set (β × β)
h : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
s₁ : Set α
s₂ : Set β
t₁ : Set α
t₂ : Set β
h₁ : (s₁, t₁) ∈ hausdorffEntourage U
h₂ : (s₂, t₂) ∈ hausdorffEntourage V
⊢ Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
    ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦ entourageProd (id i.1) (id i.2))
      (U, V))
    (((s₁, s₂), t₁, t₂).1.1 ×ˢ ((s₁, s₂), t₁, t₂).1.2, ((s₁, s₂), t₁, t₂).2.1 ×ˢ ((s₁, s₂), t₁, t₂).2.2)

Tactic:
prod_mem_hausdorffEntourage_entourageProd U V h₁ h₂

Premises used: Set.Mem, setOf, prod_mem_hausdorffEntourage_entourageProd, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
x : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))
U : Set (α × α)
V : Set (β × β)
h_1 : (U, V).1 ∈ 𝓤 α ∧ (U, V).2 ∈ 𝓤 β
hU : (U, V).1 ∈ 𝓤 α
hV : (U, V).2 ∈ 𝓤 β
h :
  ∀ (a : Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β)),
    Membership.mem (γ := Set (Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β)))
      {x : Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β) |
        x ∈ entourageProd (hausdorffEntourage (U, V).1) (hausdorffEntourage (U, V).2) →
          Membership.mem (γ := Set (Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β)))
            {x : Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β) |
              (fun (x : Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β)) ↦
                  Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
                    ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦
                        entourageProd (id i.1) (id i.2))
                      (U, V))
                    ((fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2) x.1,
                      (fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2) x.2))
                x}
            x}
      a
h₁ :
  ∀ a ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage V),
    Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
      ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦ entourageProd (id i.1) (id i.2))
        (U, V))
      (a.1.1 ×ˢ a.1.2, a.2.1 ×ˢ a.2.2)
h₂ :
  ∀ (s₁ : Set α) (s₂ : Set β) (t₁ : Set α) (t₂ : Set β) (h₁ : (s₁, t₁) ∈ hausdorffEntourage U)
    (h₂ : (s₂, t₂) ∈ hausdorffEntourage V),
    Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
      ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦ entourageProd (id i.1) (id i.2))
        (U, V))
      (((s₁, s₂), t₁, t₂).1.1 ×ˢ ((s₁, s₂), t₁, t₂).1.2, ((s₁, s₂), t₁, t₂).2.1 ×ˢ ((s₁, s₂), t₁, t₂).2.2)
⊢ ∀ᶠ (x : Prod.{u_1, u_2} (Set α) (Set β) × Prod.{u_1, u_2} (Set α) (Set β)) in 𝓤 (Prod.{u_1, u_2} (Set α) (Set β)),
    Membership.mem (γ := Set (Set (α × β) × Set (α × β)))
      ((hausdorffEntourage ∘ fun (i : Prod.{u_1, u_2} (Set (α × α)) (Set (β × β))) ↦ entourageProd (id i.1) (id i.2))
        (U, V))
      ((fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2) x.1,
        (fun (x : Prod.{u_1, u_2} (Set α) (Set β)) ↦ x.1 ×ˢ x.2) x.2)

Tactic:
filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hV)]
    with ⟨⟨s₁, s₂⟩, ⟨t₁, t₂⟩⟩ ⟨h₁, h₂⟩ using prod_mem_hausdorffEntourage_entourageProd U V h₁ h₂

Premises used: entourageProd_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
simp_rw :
  ∀ ib ∈ 𝓤 α,
    ∃ ia ∈ 𝓤 α,
      ∀ x ∈ hausdorffEntourage ia,
        closure[inst.toTopologicalSpace] x.1 ⊆ SetRel.preimage ib (closure[inst.toTopologicalSpace] x.2) ∧
          closure[inst.toTopologicalSpace] x.2 ⊆ SetRel.image ib (closure[inst.toTopologicalSpace] x.1)
⊢ UniformContinuous.{u_1, u_1} (α := Set α) closure[inst.toTopologicalSpace]

Tactic:
simp_rw [UniformContinuous, (𝓤 α).basis_sets.uniformity_hausdorff.tendsto_iff
    (𝓤 α).basis_sets.uniformity_hausdorff, Function.comp_id, mem_hausdorffEntourage]

Premises used: UniformContinuous, Function.comp_id, Filter.HasBasis.tendsto_iff, uniformity, Filter.HasBasis.uniformity_hausdorff, Filter.basis_sets, mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
obtain :
  ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U),
    ∃ ia ∈ 𝓤 α,
      ∀ x ∈ hausdorffEntourage ia,
        closure[inst.toTopologicalSpace] x.1 ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] x.2) ∧
          closure[inst.toTopologicalSpace] x.2 ⊆ SetRel.image U (closure[inst.toTopologicalSpace] x.1)
⊢ ∃ ia ∈ 𝓤 α,
    ∀ x ∈ hausdorffEntourage ia,
      closure[inst.toTopologicalSpace] x.1 ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] x.2) ∧
        closure[inst.toTopologicalSpace] x.2 ⊆ SetRel.image U (closure[inst.toTopologicalSpace] x.1)

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
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
⊢ ∃ ia ∈ 𝓤 α,
    ∀ x ∈ hausdorffEntourage ia,
      closure[inst.toTopologicalSpace] x.1 ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] x.2) ∧
        closure[inst.toTopologicalSpace] x.2 ⊆ SetRel.image U (closure[inst.toTopologicalSpace] x.1)

Tactic:
⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩

Premises used: _private.0.UniformSpace.hausdorff.uniformContinuous_closure.match_1, Prod.mk, HasSubset.Subset, Prod.fst, And, closure, And.intro, Exists.intro, SetRel.image, SetRel.preimage, Prod.snd, _private.0.UniformSpace.hausdorff.uniformContinuous_closure.match_2
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
refine :
  ∀ (x : Set α × Set α) (s t : Set α),
    (s, t) ∈ hausdorffEntourage V →
      ∀ (hst : (s, t).1 ⊆ V.preimage (s, t).2) (hts : (s, t).2 ⊆ V.image (s, t).1),
        closure[inst.toTopologicalSpace] (s, t).1 ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] (s, t).2) ∧
          closure[inst.toTopologicalSpace] (s, t).2 ⊆ SetRel.image U (closure[inst.toTopologicalSpace] (s, t).1)
⊢ ∃ ia ∈ 𝓤 α,
    ∀ x ∈ hausdorffEntourage ia,
      closure[inst.toTopologicalSpace] x.1 ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] x.2) ∧
        closure[inst.toTopologicalSpace] x.2 ⊆ SetRel.image U (closure[inst.toTopologicalSpace] x.1)

Tactic:
refine ⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h : (s, t) ∈ hausdorffEntourage V
hst : (s, t).1 ⊆ V.preimage (s, t).2
hts : (s, t).2 ⊆ V.image (s, t).1
simp :
  closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t) ∧
    closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
⊢ closure[inst.toTopologicalSpace] (s, t).1 ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] (s, t).2) ∧
    closure[inst.toTopologicalSpace] (s, t).2 ⊆ SetRel.image U (closure[inst.toTopologicalSpace] (s, t).1)

Tactic:
simp only at *
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
left : closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
right : closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t) ∧
    closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
left : V.preimage s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
left₁ : V.preimage (V.preimage t) ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
left₂ : V.preimage (V.preimage t) ⊆ SetRel.preimage U t
left₃ : V.preimage (V.preimage t) ⊆ (V.comp V).preimage t
left₄ left₅ : V.preimage (V.preimage t) ⊆ V.preimage (V.preimage t)
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)

Tactic:
grw [closure_subset_preimage hV s, hst, ← subset_closure, ← hVU, SetRel.preimage_comp]

Premises used: subset_closure, SetRel.preimage_comp, UniformSpace.closure_subset_preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
right : V.image t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
right₁ : V.image (V.image s) ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
right₂ : V.image (V.image s) ⊆ SetRel.image U s
right₃ : V.image (V.image s) ⊆ (V.comp V).image s
right₄ right₅ : V.image (V.image s) ⊆ V.image (V.image s)
⊢ closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)

Tactic:
grw [closure_subset_image hV t, hts, ← subset_closure, ← hVU, SetRel.image_comp]

Premises used: UniformSpace.closure_subset_image, subset_closure, SetRel.image_comp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Continuous[(UniformSpace.hausdorff α).toTopologicalSpace, (UniformSpace.hausdorff α).toTopologicalSpace]
    closure[inst.toTopologicalSpace]

Tactic:
uniformContinuous_closure.continuous

Premises used: UniformSpace.hausdorff.uniformContinuous_closure, UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsUniformInducing.{u_1, u_1} (α := Set α) closure[inst.toTopologicalSpace]

Tactic:
⟨le_antisymm ?_ <| Filter.map_le_iff_le_comap.mp uniformContinuous_closure⟩

Premises used: UniformSpace.hausdorff.uniformContinuous_closure, le_antisymm, IsUniformInducing.mk, Iff.mp, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
refine :
  LE.le.{u_1} (α := Filter (Set α × Set α))
    (Filter.comap (β := Set α × Set α)
      (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
      (𝓤 (Set α)))
    (𝓤 (Set α))
⊢ IsUniformInducing.{u_1, u_1} (α := Set α) closure[inst.toTopologicalSpace]

Tactic:
refine ⟨le_antisymm ?_ <| Filter.map_le_iff_le_comap.mp uniformContinuous_closure⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
rw :
  ∀ i' ∈ 𝓤 α,
    ∃ i ∈ 𝓤 α,
      (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage i ⊆
        hausdorffEntourage i'
⊢ LE.le.{u_1} (α := Filter (Set α × Set α))
    (Filter.comap (β := Set α × Set α)
      (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
      (𝓤 (Set α)))
    (𝓤 (Set α))

Tactic:
rw [(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.le_basis_iff
    (𝓤 α).basis_sets.uniformity_hausdorff, Function.comp_id]

Premises used: Function.comp_id, uniformity, Filter.HasBasis.le_basis_iff, Filter.HasBasis.uniformity_hausdorff, Filter.HasBasis.comap, Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
obtain :
  ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U),
    ∃ i ∈ 𝓤 α,
      (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage i ⊆
        hausdorffEntourage U
⊢ ∃ i ∈ 𝓤 α,
    (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
        hausdorffEntourage i ⊆
      hausdorffEntourage U

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
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
⊢ ∃ i ∈ 𝓤 α,
    (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
        hausdorffEntourage i ⊆
      hausdorffEntourage U

Tactic:
⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩

Premises used: _private.0.UniformSpace.hausdorff.isUniformInducing_closure.match_1, Membership.mem, _private.0.UniformSpace.hausdorff.isUniformInducing_closure.match_2, Prod.mk, And.intro, Exists.intro, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
refine :
  ∀ (x : Set α × Set α) (s t : Set α),
    Membership.mem (γ := Set (Set α × Set α))
        ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
          hausdorffEntourage V)
        (s, t) →
      ∀
        (hst :
          ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
                (s, t)).1 ⊆
            V.preimage
              ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
                  (s, t)).2)
        (hts :
          ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
                (s, t)).2 ⊆
            V.image
              ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
                  (s, t)).1),
        (s, t) ∈ hausdorffEntourage U
⊢ ∃ i ∈ 𝓤 α,
    (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
        hausdorffEntourage i ⊆
      hausdorffEntourage U

Tactic:
refine ⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h :
  Membership.mem (γ := Set (Set α × Set α))
    ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
      hausdorffEntourage V)
    (s, t)
hst :
  ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) (s, t)).1 ⊆
    V.preimage
      ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
          (s, t)).2
hts :
  ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) (s, t)).2 ⊆
    V.image
      ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2))
          (s, t)).1
simp : s ⊆ SetRel.preimage U t ∧ t ⊆ SetRel.image U s
⊢ (s, t) ∈ hausdorffEntourage U

Tactic:
simp only [mem_hausdorffEntourage] at *

Premises used: mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h :
  Membership.mem (γ := Set (Set α × Set α))
    ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
      hausdorffEntourage V)
    (s, t)
hst : closure[inst.toTopologicalSpace] s ⊆ V.preimage (closure[inst.toTopologicalSpace] t)
hts : closure[inst.toTopologicalSpace] t ⊆ V.image (closure[inst.toTopologicalSpace] s)
left : s ⊆ SetRel.preimage U t
right : t ⊆ SetRel.image U s
⊢ s ⊆ SetRel.preimage U t ∧ t ⊆ SetRel.image U s

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x : Set α × Set α
s t : Set α
h :
  Membership.mem (γ := Set (Set α × Set α))
    ((fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
      hausdorffEntourage V)
    (s, t)
hst : closure[inst.toTopologicalSpace] s ⊆ V.preimage (closure[inst.toTopologicalSpace] t)
hts : closure[inst.toTopologicalSpace] t ⊆ V.image (closure[inst.toTopologicalSpace] s)
left : closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U t
left₁ : V.preimage (closure[inst.toTopologicalSpace] t) ⊆ SetRel.preimage U t
left₂ : V.preimage (V.preimage t) ⊆ SetRel.preimage U t
left₃ : V.preimage (V.preimage t) ⊆ (V.comp V).preimage t
left₄ left₅ : V.preimage (V.preimage t) ⊆ V.preimage (V.preimage t)
⊢ s ⊆ SetRel.preimage U t

Tactic:
grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]

Premises used: subset_closure, SetRel.preimage_comp, UniformSpace.closure_subset_preimage