-- 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
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
simp_rw :
  UniformSpace.comap F
      (⨅ s ∈ 𝔖,
        UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑s : Type u_2) α)
          (Function.comp (β := (↑s : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α) :
              (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α)
            (Function.comp (β := X → α) (s.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑s : Type u_2) → α))
          (UniformFun.uniformSpace (↑s : Type u_2) α)) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
simp_rw₁ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap F
        (UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
          (Function.comp (β := (↑i : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α))
          (UniformFun.uniformSpace (↑i : Type u_2) α)))
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
simp_rw₂ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (Function.comp (β := (↑i : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α) ∘
          F)
        (UniformFun.uniformSpace (↑i : Type u_2) α))
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
simp_rw₃ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (Function.comp (β := (↑i : Type u_2) → α)
            ((⇑{ toFun := fun (x : (↑i : Type u_2) → α) ↦ x,
                    invFun := fun (x : UniformFun.{u_2, u_3} (↑i : Type u_2) α) ↦ x, left_inv := ⋯, right_inv := ⋯ } :
                (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α) ∘
          F)
        (UniformFun.uniformSpace (↑i : Type u_2) α))
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
simp_rw₄ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (Function.comp (β := (↑i : Type u_2) → α) (fun (x : (↑i : Type u_2) → α) ↦ x)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α) ∘
          F)
        (UniformFun.uniformSpace (↑i : Type u_2) α))
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
simp_rw₅ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (Function.comp (β := (↑i : Type u_2) → α) (fun (x : (↑i : Type u_2) → α) ↦ x)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(Equiv.symm (UniformOnFun.ofFun 𝔖)) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α) ∘
          F)
        (UniformFun.uniformSpace (↑i : Type u_2) α))
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
have simp_rw₆ : Eq.{u_1 + 1} (α := UniformSpace ι)
  (⨅ i ∈ 𝔖,
    UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
      (Function.comp (β := (↑i : Type u_2) → α) (fun (x : (↑i : Type u_2) → α) ↦ x)
          (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
              (⇑(Equiv.symm
                    { toFun := fun (x : X → α) ↦ x, invFun := fun (x : X →ᵤ[𝔖] α) ↦ x, left_inv := sorry,
                      right_inv := sorry }) :
                (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α) ∘
        F)
      (UniformFun.uniformSpace (↑i : Type u_2) α))
  (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
Tactic: simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap,
      UniformFun.ofFun, Equiv.coe_fn_mk, UniformOnFun.toFun, UniformOnFun.ofFun, Function.comp_def,
      UniformFun, Equiv.coe_fn_symm_mk]