awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
have 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)
Tactic: refine (𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets |>.lift' monotone_hausdorffEntourage
    |>.tendsto_right_iff.mpr fun ⟨U, V⟩ ⟨hU, hV⟩ => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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 β
⊢ ((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)
have 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)
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 β
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 ∈ 𝓤 β
⊢ ∀ᶠ (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)
have 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
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₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ ∀ᶠ (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)
have 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)
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₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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)
⊢ ∀ᶠ (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)
have 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)
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₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous.{u_1, u_1} (α := Set α) closure[inst.toTopologicalSpace]
have 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)
Tactic: simp_rw [UniformContinuous, (𝓤 α).basis_sets.uniformity_hausdorff.tendsto_iff
    (𝓤 α).basis_sets.uniformity_hausdorff, Function.comp_id, mem_hausdorffEntourage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : 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)
have 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)
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 α
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)
have 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)
Tactic: refine ⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩
-- 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 : (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)
have simp : closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t) ∧
  closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
Tactic: simp only 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 : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t) ∧
    closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have left : closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] 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 : (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)
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t) ∧
    closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have right : closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] 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 : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
have left : V.preimage s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
Tactic: grw [closure_subset_preimage hV s, hst, ← subset_closure, ← 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 : (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)
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
have left₁ : V.preimage (V.preimage t) ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
Tactic: grw [closure_subset_preimage hV s, hst, ← subset_closure, ← 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 : (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)
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
have left₂ : V.preimage (V.preimage t) ⊆ SetRel.preimage U t
Tactic: grw [closure_subset_preimage hV s, hst, ← subset_closure, ← 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 : (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
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
have left₃ : V.preimage (V.preimage t) ⊆ (V.comp V).preimage t
Tactic: grw [closure_subset_preimage hV s, hst, ← subset_closure, ← 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 : (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
⊢ closure[inst.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst.toTopologicalSpace] t)
have left₄ : V.preimage (V.preimage t) ⊆ V.preimage (V.preimage t)
Tactic: grw [closure_subset_preimage hV s, hst, ← subset_closure, ← 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 : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have right : V.image t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
Tactic: grw [closure_subset_image hV t, hts, ← subset_closure, ← 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 : (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)
⊢ closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have right₁ : V.image (V.image s) ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
Tactic: grw [closure_subset_image hV t, hts, ← subset_closure, ← 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 : (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)
⊢ closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have right₂ : V.image (V.image s) ⊆ SetRel.image U s
Tactic: grw [closure_subset_image hV t, hts, ← subset_closure, ← 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 : (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
⊢ closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have right₃ : V.image (V.image s) ⊆ (V.comp V).image s
Tactic: grw [closure_subset_image hV t, hts, ← subset_closure, ← 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 : (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
⊢ closure[inst.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst.toTopologicalSpace] s)
have right₄ : V.image (V.image s) ⊆ V.image (V.image s)
Tactic: grw [closure_subset_image hV t, hts, ← subset_closure, ← hVU, SetRel.image_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsUniformInducing.{u_1, u_1} (α := Set α) closure[inst.toTopologicalSpace]
have 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 α))
Tactic: refine ⟨le_antisymm ?_ <| Filter.map_le_iff_le_comap.mp uniformContinuous_closure⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ 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 α))
have rw : ∀ i' ∈ 𝓤 α,
  ∃ i ∈ 𝓤 α,
    (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
        hausdorffEntourage i ⊆
      hausdorffEntourage i'
Tactic: rw [(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.le_basis_iff
    (𝓤 α).basis_sets.uniformity_hausdorff, Function.comp_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ i ∈ 𝓤 α,
    (fun (x : Set α × Set α) ↦ (closure[inst.toTopologicalSpace] x.1, closure[inst.toTopologicalSpace] x.2)) ⁻¹'
        hausdorffEntourage i ⊆
      hausdorffEntourage U
have 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
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 α
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
have 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
Tactic: refine ⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩