-- Module: Mathlib.Topology.UniformSpace.Ascoli
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) α))
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 := ⋯,
                        right_inv := ⋯ }) :
                  (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) α)
        (fun (x : ι) ↦
          i.restrict (π := fun (a : X) ↦ α)
            ((Equiv.symm
                  { toFun := fun (x : X → α) ↦ x, invFun := fun (x : X →ᵤ[𝔖] α) ↦ x, left_inv := ⋯, right_inv := ⋯ } :
                (a : X →ᵤ[𝔖] α) → X → α)
              (F x)))
        (UniformFun.uniformSpace (↑i : Type u_2) α))
    (⨅ K ∈ 𝔖,
      UniformSpace.comap (β := (a : (↑K : Type u_2)) → α) (fun (x : ι) ↦ K.restrict (π := fun (a : X) ↦ α) (F x))
        (UniformFun.uniformSpace (↑K : Type u_2) α))
simp_rw₈ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := (↑i : Type u_2) → α)
        (fun (x : ι) ↦
          i.restrict (π := fun (a : X) ↦ α)
            ((Equiv.symm
                  { toFun := fun (x : X → α) ↦ x, invFun := fun (x : X →ᵤ[𝔖] α) ↦ x, left_inv := ⋯, right_inv := ⋯ } :
                (a : X →ᵤ[𝔖] α) → X → α)
              (F x)))
        (UniformFun.uniformSpace (↑i : Type u_2) α))
    (⨅ K ∈ 𝔖,
      UniformSpace.comap (β := (a : (↑K : Type u_2)) → α) (fun (x : ι) ↦ K.restrict (π := fun (a : X) ↦ α) (F x))
        (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) α)

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]

Premises used: Equiv.coe_fn_symm_mk, UniformOnFun.uniformSpace, UniformOnFun.toFun, UniformSpace.comap_comap, Function.comp_def, UniformFun, UniformSpace.comap_iInf, Equiv.coe_fn_mk, UniformOnFun.ofFun, UniformFun.ofFun