awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ (s, t) ∈ hausdorffEntourage U
have simp : s ⊆ SetRel.preimage U t ∧ t ⊆ SetRel.image U s
Tactic: simp only [mem_hausdorffEntourage] at *
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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)
⊢ s ⊆ SetRel.preimage U t ∧ t ⊆ SetRel.image U s
have left : s ⊆ SetRel.preimage U t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ s ⊆ SetRel.preimage U t ∧ t ⊆ SetRel.image U s
have right : t ⊆ SetRel.image U s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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)
⊢ s ⊆ SetRel.preimage U t
have left : closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U t
Tactic: grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ s ⊆ SetRel.preimage U t
have left₁ : V.preimage (closure[inst.toTopologicalSpace] t) ⊆ SetRel.preimage U t
Tactic: grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ s ⊆ SetRel.preimage U t
have left₂ : V.preimage (V.preimage t) ⊆ SetRel.preimage U t
Tactic: grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ s ⊆ SetRel.preimage U t
have left₃ : V.preimage (V.preimage t) ⊆ (V.comp V).preimage t
Tactic: grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ s ⊆ SetRel.preimage U t
have left₄ : V.preimage (V.preimage t) ⊆ V.preimage (V.preimage t)
Tactic: grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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)
⊢ t ⊆ SetRel.image U s
have right : closure[inst.toTopologicalSpace] t ⊆ SetRel.image U s
Tactic: grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ t ⊆ SetRel.image U s
have right₁ : V.image (closure[inst.toTopologicalSpace] s) ⊆ SetRel.image U s
Tactic: grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ t ⊆ SetRel.image U s
have right₂ : V.image (V.image s) ⊆ SetRel.image U s
Tactic: grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ t ⊆ SetRel.image U s
have right₃ : V.image (V.image s) ⊆ (V.comp V).image s
Tactic: grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ t ⊆ SetRel.image U s
have right₄ : V.image (V.image s) ⊆ V.image (V.image s)
Tactic: grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
⊢ 𝓝 (closure[inst.toTopologicalSpace] s) = 𝓝 s
have simp_rw : Filter.comap closure[inst.toTopologicalSpace]
    (𝓝 (closure[inst.toTopologicalSpace] (closure[inst.toTopologicalSpace] s))) =
  Filter.comap closure[inst.toTopologicalSpace] (𝓝 (closure[inst.toTopologicalSpace] s))
Tactic: simp_rw +singlePass [isUniformInducing_closure.isInducing.nhds_eq_comap, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {s : Set α | TotallyBounded s}
have 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
Tactic: simp_rw [isClosed_iff_frequently, nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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 ∈ 𝓤 α
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
have obtain : ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U), ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
Tactic: obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
have 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}
Tactic: rw [(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.frequently_iff] at hs
Cleared hypotheses: hs, U, hU, V, hV, hVU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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 α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
have 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}
Tactic: obtain ⟨t, ⟨hst : s ⊆ V.preimage t, -⟩, ht⟩ := hs V hV
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
have 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}
Tactic: obtain ⟨u, hu, htu⟩ := ht V hV
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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}
have refine : s ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
Tactic: refine ⟨u, hu, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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}
⊢ s ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ U}
have grw : V.preimage (⋃ y ∈ u, {x : α | (x, y) ∈ V}) ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V.comp V}
Tactic: grw [hst, htu, ← hVU]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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}
⊢ V.preimage (⋃ y ∈ u, {x : α | (x, y) ∈ V}) ⊆ ⋃ y ∈ u, {x : α | (x, y) ∈ V.comp V}
have 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
Tactic: simp [Set.subset_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : DiscreteUniformity α
⊢ DiscreteUniformity.{u_1} (Set α)
have rw : Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) SetRel.id
Tactic: rw [discreteUniformity_iff_setRelId_mem_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : DiscreteUniformity α
⊢ Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) SetRel.id
have h : Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) SetRel.id (hausdorffEntourage SetRel.id)
Tactic: convert! Filter.mem_lift' (DiscreteUniformity.relId_mem_uniformity α)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : DiscreteUniformity α
⊢ Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) SetRel.id (hausdorffEntourage SetRel.id)
have h : Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) SetRel.id SetRel.id
Tactic: rw [hausdorffEntourage_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
have 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
Tactic: refine Filter.tendsto_lift'.mpr fun U hU => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
U : Set (β × β)
hU : U ∈ 𝓤 β
s t : Set α
⊢ 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
have 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
Tactic: ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
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
have 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
Tactic: filter_upwards [Filter.mem_lift' (hf hU)] with ⟨s, t⟩ ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ (f '' (s, t).1, f '' (s, t).2) ∈ hausdorffEntourage U
have h : s ⊆ f ⁻¹' SetRel.preimage U (f '' t) ∧ t ⊆ f ⁻¹' SetRel.image U (f '' s)
Tactic: simp_rw [mem_hausdorffEntourage, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ IsUniformInducing.{u_1, u_2} (β := Set β) fun (x : Set α) ↦ f '' x
have 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 α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ Filter.comap (fun (x : Set α × Set α) ↦ (f '' x.1, f '' x.2)) ((𝓤 β).lift' hausdorffEntourage) =
    (𝓤 α).lift' hausdorffEntourage
have 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)))
Tactic: rw [Filter.comap_lift'_eq, ← hf.comap_uniformity,
    Filter.comap_lift'_eq2 monotone_hausdorffEntourage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ 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)))
have 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)
Tactic: congr with U ⟨s, t⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ TotallyBounded (𝒫 t)
have 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
Tactic: simp_rw [(𝓤 α).basis_sets.uniformity_hausdorff.totallyBounded_iff, Function.comp_id,
    Set.powerset, Set.setOf_subset, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
t : Set α
ht : TotallyBounded t
U : SetRel α α
hU : 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
have 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
Tactic: obtain ⟨u, hu, ht⟩ := ht U hU