-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
simp_rw :
  (∀ (a : X →ᵤ[𝔖] α),
      ClusterPt a (𝓟 (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), ClusterPt a (𝓟 (range F)) → a ∈ range F
simp_rw₁ :
  (∀ (a : X →ᵤ[𝔖] α),
      ClusterPt a (map ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ⊤) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), ClusterPt a (map F ⊤) → a ∈ range F
simp_rw₂ :
  (∀ (a : X →ᵤ[𝔖] α),
      MapClusterPt a ⊤ ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), MapClusterPt a ⊤ F → a ∈ range F
simp_rw₃ :
  (∀ (a : X →ᵤ[𝔖] α),
      (∃ (U : Ultrafilter ι),
          (↑U : Filter ι) ≤ ⊤ ∧
            Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → a ∈ range F
simp_rw₄ :
  (∀ (a : X →ᵤ[𝔖] α),
      (∃ (U : Ultrafilter ι),
          (↑U : Filter ι) ≤ ⊤ ∧
            Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) '' range F) a) ↔
    ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → a ∈ range F
simp_rw₅ :
  (∀ (x : X → α),
      (∃ (U : Ultrafilter ι),
          (↑U : Filter ι) ≤ ⊤ ∧
            Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α)
              (↑U : Filter ι) (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x) : Filter (X →ᵤ[𝔖] α))) →
        Membership.mem (α := X →ᵤ[𝔖] α) (γ := Set (X →ᵤ[𝔖] α))
          ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) '' range F)
          ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x : X →ᵤ[𝔖] α)) ↔
    ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → a ∈ range F
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw₆ : (∀ (x : X → α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧
          Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α)
            (↑U : Filter ι) (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x) : Filter (X →ᵤ[𝔖] α))) →
      Membership.mem (α := X →ᵤ[𝔖] α) (γ := Set (X →ᵤ[𝔖] α))
        ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) '' range F)
        ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x : X →ᵤ[𝔖] α)) ↔
  ∀ (a : X → α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧
          Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α)
            (↑U : Filter ι) (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) a) : Filter (X →ᵤ[𝔖] α))) →
      a ∈ range F
Tactic: simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
    mapClusterPt_iff_ultrafilter, range_comp, (UniformOnFun.ofFun 𝔖).surjective.forall,
    ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
    (UniformOnFun.ofFun 𝔖).injective.mem_set_image]