-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
open : 𝓝 s ≤ Filter.comap (Prod.mk s) (𝓤 (Set α))
open₁ :
  ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i' ∈ 𝓝 s
open₂ : ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' hausdorffEntourage i' ∈ 𝓝 s
open₃ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      Prod.mk s ⁻¹' {x : Set α × Set α | x.1 ⊆ i'.preimage x.2 ∧ x.2 ⊆ i'.image x.1} ∈ 𝓝 s
open₄ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a : Set α | s ⊆ i'.preimage a ∧ a ⊆ i'.image s} ∈ 𝓝 s
open₅ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      {a : Set α | s ⊆ i'.preimage a} ∩ {a : Set α | a ⊆ i'.image s} ∈ 𝓝 s
open₆ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₇ open₈ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₉ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
open₁₀ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl) (V : SetRel α α)
    (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
    V.IsSymm → ∀ (hVU : V.comp V ⊆ U), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
open₁₁ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl) (V : SetRel α α)
    (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
    V.IsSymm →
      ∀ (hVU : V.comp V ⊆ U) (t : Finset α) (ht₁ : ((↑t : Set α), s).1 ⊆ V.preimage ((↑t : Set α), s).2)
        (ht₂ : ((↑t : Set α), s).2 ⊆ V.image ((↑t : Set α), s).1), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
⊢ 𝓝 s ≤ 𝓝 s
have open₁₂ : ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl) (V : SetRel α α)
  (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
  V.IsSymm →
    ∀ (hVU : V.comp V ⊆ U) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ V.preimage s) (ht₂ : s ⊆ V.image (↑t : Set α)),
      {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
Tactic: open UniformSpace TopologicalSpace.vietoris in
  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]
  intro U ⟨hU₁, hU₂⟩
  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
  let := TopologicalSpace.vietoris α
  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _
  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
  dsimp only at ht₁ ht₂
  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]