awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
right : closure[inst.toTopologicalSpace] t ⊆ SetRel.image U s
right₁ : V.image (closure[inst.toTopologicalSpace] s) ⊆ SetRel.image U 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)
⊢ t ⊆ SetRel.image U s

Tactic:
grw [subset_closure (s := t), hts, closure_subset_image hV s, ← 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 α
s : Set α
simp_rw :
  Filter.comap closure[inst.toTopologicalSpace]
      (𝓝 (closure[inst.toTopologicalSpace] (closure[inst.toTopologicalSpace] s))) =
    Filter.comap closure[inst.toTopologicalSpace] (𝓝 (closure[inst.toTopologicalSpace] s))
⊢ 𝓝 (closure[inst.toTopologicalSpace] s) = 𝓝 s

Tactic:
simp_rw +singlePass [isUniformInducing_closure.isInducing.nhds_eq_comap, closure_closure]

Premises used: Topology.IsInducing.nhds_eq_comap, IsUniformInducing.isInducing, UniformSpace.hausdorff.isUniformInducing_closure, closure_closure
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
simp_rw :
  ∀ (x : Set α),
    (∃ᶠ (y : Set α) in Filter.comap (Prod.mk x) (𝓤 (Set α)),
        Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} y) →
      Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {s : Set α | TotallyBounded s}

Tactic:
simp_rw [isClosed_iff_frequently, nhds_eq_comap_uniformity]

Premises used: isClosed_iff_frequently, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∃ᶠ (y : Set α) in Filter.comap (Prod.mk s) (𝓤 (Set α)),
    Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} y
U : Set (α × α)
hU : U ∈ 𝓤 α
obtain :
  ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U), ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ 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 α
s : Set α
hs :
  ∃ᶠ (y : Set α) in Filter.comap (Prod.mk s) (𝓤 (Set α)),
    Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} y
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
rw :
  ∀
    (hs :
      ∀ i ∈ 𝓤 α,
        ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i,
          Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x)
    (U : Set (α × α)) (hU : U ∈ 𝓤 α) (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U),
    ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
rw [(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.frequently_iff] at hs

Premises used: uniformity, Filter.HasBasis.uniformity_hausdorff, Filter.HasBasis.comap, Filter.basis_sets, Filter.HasBasis.frequently_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
obtain :
  ∀ (t : Set α) (ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t) (hst : s ⊆ V.preimage t),
    ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
obtain ⟨t, ⟨hst : s ⊆ V.preimage t, -⟩, ht⟩ := hs V hV
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t
hst : s ⊆ V.preimage t
obtain :
  ∀ (u : Set α) (hu : u.Finite) (htu : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V}),
    ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
obtain ⟨u, hu, htu⟩ := ht V hV
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V}
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
⟨u, hu, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V}
refine : s ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
refine ⟨u, hu, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V}
grw : V.preimage (⋃ y ∈ u, {x : α | (x, y) ∈ V}) ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V.comp V}
⊢ s ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}

Tactic:
grw [hst, htu, ← hVU]
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V}
simp : ∀ (x x_1 x_2 : α), x_2 ∈ u → (x_1, x_2) ∈ V → (x, x_1) ∈ V → ∃ i ∈ u, ∃ (b : α), (x, b) ∈ V ∧ (b, i) ∈ V
⊢ V.preimage (⋃ y ∈ u, {x : α | (x, y) ∈ V}) ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V.comp V}

Tactic:
simp [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs :
  ∀ i ∈ 𝓤 α,
    ∃ x ∈ Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i, Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} x
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | TotallyBounded s} t
hst : s ⊆ V.preimage t
u : Set α
hu : u.Finite
htu : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V}
⊢ ∀ (x x_1 x_2 : α), x_2 ∈ u → (x_1, x_2) ∈ V → (x, x_1) ∈ V → ∃ i ∈ u, ∃ (b : α), (x, b) ∈ V ∧ (b, i) ∈ V

Tactic:
grind
-- 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 α
rw : Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) SetRel.id
⊢ DiscreteUniformity.{u_1} (Set α)

Tactic:
rw [discreteUniformity_iff_setRelId_mem_uniformity]

Premises used: discreteUniformity_iff_setRelId_mem_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 : DiscreteUniformity α
⊢ hausdorffEntourage SetRel.id ∈ (𝓤 α).lift' hausdorffEntourage

Tactic:
Filter.mem_lift' (DiscreteUniformity.relId_mem_uniformity α)

Premises used: Filter.mem_lift', DiscreteUniformity.relId_mem_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 : DiscreteUniformity α
h : Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) SetRel.id (hausdorffEntourage SetRel.id)
⊢ Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) SetRel.id

Tactic:
convert! Filter.mem_lift' (DiscreteUniformity.relId_mem_uniformity α)

Premises used: Filter.mem_lift', DiscreteUniformity.relId_mem_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 : DiscreteUniformity α
h h₁ : Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) SetRel.id SetRel.id
⊢ Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) SetRel.id (hausdorffEntourage SetRel.id)

Tactic:
rw [hausdorffEntourage_id]

Premises used: hausdorffEntourage_id
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous.{u_1, u_2} (β := Set β) fun (x : Set α) ↦ f '' x

Tactic:
Filter.tendsto_lift'.mpr fun U hU => ?_

Premises used: Iff.mpr, Filter.tendsto_lift', UniformContinuous, iInf, uniformity, Filter.lift', Filter.lift
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
refine :
  ∀ (U : Set (β × β)) (hU : U ∈ 𝓤 β),
    ∀ᶠ (a : Set α × Set α) in 𝓤 (Set α),
      ((fun (x : Set α) ↦ f '' x) a.1, (fun (x : Set α) ↦ f '' x) a.2) ∈ hausdorffEntourage U
⊢ UniformContinuous.{u_1, u_2} (β := Set β) fun (x : Set α) ↦ f '' x

Tactic:
refine Filter.tendsto_lift'.mpr fun U hU => ?_

Premises used: Iff.mpr, Filter.tendsto_lift'
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h :
  ∀ (h₁ : (s, t).1 ⊆ SetRel.preimage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2)
    (h₂ : (s, t).2 ⊆ SetRel.image ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1),
    (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U
⊢ Membership.mem (γ := Set (Set α × Set α)) (hausdorffEntourage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U)) (s, t) →
    (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U

Tactic:
⟨h₁, h₂⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
h :
  ∀ (s t : Set α) (h₁ : (s, t).1 ⊆ SetRel.preimage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2)
    (h₂ : (s, t).2 ⊆ SetRel.image ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1),
    (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U
⊢ ∀ᶠ (a : Set α × Set α) in 𝓤 (Set α),
    ((fun (x : Set α) ↦ f '' x) a.1, (fun (x : Set α) ↦ f '' x) a.2) ∈ hausdorffEntourage U

Tactic:
filter_upwards [Filter.mem_lift' (hf hU)] with ⟨s, t⟩ ⟨h₁, h₂⟩

Premises used: Filter.mem_lift'
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h₁ : (s, t).1 ⊆ SetRel.preimage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2
h₂ : (s, t).2 ⊆ SetRel.image ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1
h : s ⊆ f ⁻¹' SetRel.preimage U (f '' t) ∧ t ⊆ f ⁻¹' SetRel.image U (f '' s)
⊢ (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U

Tactic:
simp_rw [mem_hausdorffEntourage, Set.image_subset_iff]

Premises used: mem_hausdorffEntourage, Set.image_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h₁ : (s, t).1 ⊆ SetRel.preimage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2
h₂ : (s, t).2 ⊆ SetRel.image ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1
⊢ s ⊆ f ⁻¹' SetRel.preimage U (f '' t) ∧ t ⊆ f ⁻¹' SetRel.image U (f '' s)

Tactic:
⟨h₁.trans fun x ⟨y, hy, hxy⟩ => ⟨f y, Set.mem_image_of_mem f hy, hxy⟩,
    h₂.trans fun x ⟨y, hy, hxy⟩ => ⟨f y, Set.mem_image_of_mem f hy, hxy⟩⟩

Premises used: _private.0.UniformContinuous.image_hausdorff.match_3, Membership.mem, HasSubset.Subset.trans, Set.preimage, Set.mem_image_of_mem, And.intro, Exists.intro, Set.image, SetRel.image, SetRel.preimage, _private.0.UniformContinuous.image_hausdorff.match_2
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
h₁ : (s, t).1 ⊆ SetRel.preimage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).2
h₂ : (s, t).2 ⊆ SetRel.image ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' U) (s, t).1
⊢ s ⊆ f ⁻¹' SetRel.preimage U (f '' t) ∧ t ⊆ f ⁻¹' SetRel.image U (f '' s)

Tactic:
exact ⟨h₁.trans fun x ⟨y, hy, hxy⟩ => ⟨f y, Set.mem_image_of_mem f hy, hxy⟩,
    h₂.trans fun x ⟨y, hy, hxy⟩ => ⟨f y, Set.mem_image_of_mem f hy, hxy⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
comap_uniformity :
  Eq.{u_1 + 1} (α := Filter (Set α × Set α))
    (Filter.comap.{u_1, u_2} (β := Set β × Set β) (fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) (𝓤 (Set β)))
    (𝓤 (Set α))
⊢ IsUniformInducing.{u_1, u_2} (β := Set β) fun (x : Set α) ↦ f '' x

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
comap_uniformity :
  Eq.{u_1 + 1} (α := Filter (Set α × Set α))
    ((𝓤 β).lift' ((Set.preimage fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) ∘ hausdorffEntourage))
    ((𝓤 β).lift' (hausdorffEntourage ∘ Set.preimage fun (x : α × α) ↦ (f x.1, f x.2)))
⊢ Filter.comap (fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) ((𝓤 β).lift' hausdorffEntourage) =
    (𝓤 α).lift' hausdorffEntourage

Tactic:
rw [Filter.comap_lift'_eq, ← hf.comap_uniformity,
    Filter.comap_lift'_eq2 monotone_hausdorffEntourage]

Premises used: IsUniformInducing.comap_uniformity, monotone_hausdorffEntourage, Filter.comap_lift'_eq, Filter.comap_lift'_eq2
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
comap_uniformity :
  ∀ (U : Set (β × β)) (s t : Set α),
    Membership.mem (γ := Set (Set α × Set α))
        (((Set.preimage fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) ∘ hausdorffEntourage) U) (s, t) ↔
      Membership.mem (γ := Set (Set α × Set α)) ((hausdorffEntourage ∘ Set.preimage fun (x : α × α) ↦ (f x.1, f x.2)) U)
        (s, t)
⊢ Eq.{u_1 + 1} (α := Filter (Set α × Set α))
    ((𝓤 β).lift' ((Set.preimage fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) ∘ hausdorffEntourage))
    ((𝓤 β).lift' (hausdorffEntourage ∘ Set.preimage fun (x : α × α) ↦ (f x.1, f x.2)))

Tactic:
congr with U ⟨s, t⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
U : Set (β × β)
s t : Set α
⊢ Membership.mem (γ := Set (Set α × Set α))
      (((Set.preimage fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) ∘ hausdorffEntourage) U) (s, t) ↔
    Membership.mem (γ := Set (Set α × Set α)) ((hausdorffEntourage ∘ Set.preimage fun (x : α × α) ↦ (f x.1, f x.2)) U)
      (s, t)

Tactic:
simp only [Function.comp, hausdorffEntourage, SetRel.preimage, SetRel.image, Set.preimage,
    Set.mem_setOf, Set.image_subset_iff, Set.exists_mem_image]

Premises used: Function.comp, Set.mem_setOf, Set.preimage, Set.exists_mem_image, SetRel.image, SetRel.preimage, Set.image_subset_iff, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
simp_rw :
  ∀ i ∈ 𝓤 α,
    ∃ (t_1 : Set (Set α)),
      t_1.Finite ∧
        ∀ x ⊆ t,
          ∃ (i_1 : Set α) (_ : i_1 ∈ t_1),
            Membership.mem (γ := Set (Set α)) {x : Set α | (x, i_1) ∈ hausdorffEntourage i} x
⊢ TotallyBounded (𝒫 t)

Tactic:
simp_rw [(𝓤 α).basis_sets.uniformity_hausdorff.totallyBounded_iff, Function.comp_id,
    Set.powerset, Set.setOf_subset, Set.mem_iUnion]

Premises used: Function.comp_id, uniformity, Set.mem_iUnion, Set.powerset, Filter.HasBasis.uniformity_hausdorff, Set.setOf_subset, Filter.basis_sets, Filter.HasBasis.totallyBounded_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
obtain :
  ∀ (u : Set α) (hu : u.Finite) (ht : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}),
    ∃ (t_1 : Set (Set α)),
      t_1.Finite ∧
        ∀ x ⊆ t,
          ∃ (i : Set α) (_ : i ∈ t_1), Membership.mem (γ := Set (Set α)) {x : Set α | (x, i) ∈ hausdorffEntourage U} x
⊢ ∃ (t_1 : Set (Set α)),
    t_1.Finite ∧
      ∀ x ⊆ t,
        ∃ (i : Set α) (_ : i ∈ t_1), Membership.mem (γ := Set (Set α)) {x : Set α | (x, i) ∈ hausdorffEntourage U} x

Tactic:
obtain ⟨u, hu, ht⟩ := ht U hU
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht_1 : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
s : Set α
hs : s ⊆ t
⊢ u ∩ U.image s ∈ 𝒫 u

Tactic:
grind
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht_1 : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
refine : ∀ (s : Set α) (hs : s ⊆ t) (x : α) (hx : x ∈ (s, u ∩ U.image s).1), x ∈ U.preimage (s, u ∩ U.image s).2
⊢ ∃ (t_1 : Set (Set α)),
    t_1.Finite ∧
      ∀ x ⊆ t,
        ∃ (i : Set α) (_ : i ∈ t_1), Membership.mem (γ := Set (Set α)) {x : Set α | (x, i) ∈ hausdorffEntourage U} x

Tactic:
refine ⟨u.powerset, hu.powerset, fun s hs => ⟨u ∩ U.image s, by grind, fun x hx => ?_,
    fun x ⟨_, hx⟩ => hx⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht_1 : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
s : Set α
hs : s ⊆ t
x : α
hx : x ∈ (s, u ∩ U.image s).1
obtain :
  ∀ (y : α) (hy : y ∈ u) (hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ U} x), x ∈ U.preimage (s, u ∩ U.image s).2
⊢ x ∈ U.preimage (s, u ∩ U.image s).2

Tactic:
obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht (hs hx))

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht_1 : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
s : Set α
hs : s ⊆ t
x : α
hx : x ∈ (s, u ∩ U.image s).1
y : α
hy : y ∈ u
hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ U} x
⊢ x ∈ U.preimage (s, u ∩ U.image s).2

Tactic:
⟨y, ⟨hy, ⟨x, hx, hxy⟩⟩, hxy⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, SetRel.preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht_1 : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
u : Set α
hu : u.Finite
ht : t ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
s : Set α
hs : s ⊆ t
x : α
hx : x ∈ (s, u ∩ U.image s).1
y : α
hy : y ∈ u
hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ U} x
⊢ x ∈ U.preimage (s, u ∩ U.image s).2

Tactic:
exact ⟨y, ⟨hy, ⟨x, hx, hxy⟩⟩, hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
simp_rw :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      {a : Set α | s ⊆ i'.preimage a} ∩ {a : Set α | a ⊆ i'.image s} ∈ 𝓝 s
⊢ 𝓝 s ≤ 𝓝 s

Tactic:
simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_setOf_eq, Set.setOf_and]

Premises used: Function.comp_id, Set.setOf_and, Filter.HasBasis.uniformity_hausdorff, Filter.HasBasis.ge_iff, Filter.HasBasis.comap, Set.preimage_setOf_eq, nhds_eq_comap_uniformity, uniformity_hasBasis_open, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
this :
  ∀ (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
⊢ U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U → {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s

Tactic:
⟨hU₁, hU₂⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
⊢ U.IsRefl

Tactic:
have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
-- 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 α
⊢ {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s

Tactic:
Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _

Premises used: Filter.inter_mem, SetRel.self_subset_image, IsOpen.powerset_vietoris, IsOpen.mem_nhds, IsOpen.relImage
-- 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 α
refine : {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
⊢ {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s

Tactic:
refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _

Premises used: Filter.inter_mem, SetRel.self_subset_image, IsOpen.powerset_vietoris, IsOpen.mem_nhds, IsOpen.relImage
-- 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 α
obtain :
  ∀ (V : SetRel α α) (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
    V.IsSymm → ∀ (hVU : V.comp V ⊆ U), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
⊢ {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s

Tactic:
obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁

Premises used: SetRel, comp_open_symm_mem_uniformity_sets