-- 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
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace.{u_2} (↑K : Type u_2)
a :
  Tendsto (β := UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      (Function.comp (β := X →ᵤ[𝔖] α)
        (Function.comp (β := (↑K : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
            (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
          (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α))
        ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
      ℱ
      (𝓝
        (Function.comp (α := X →ᵤ[𝔖] α) (β := (↑K : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
            (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
          (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α)
          ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f : X →ᵤ[𝔖] α))) ↔
    Tendsto (β := UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → (↑K : Type u_2) →ᵤ α) ∘ K.restrict (π := fun (a : X) ↦ α) ∘ F :
        ι → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      ℱ
      (𝓝 ((UniformFun.ofFun : (a : (↑K : Type u_2) → α) → (↑K : Type u_2) →ᵤ α) (K.restrict (π := fun (x : X) ↦ α) f)) :
        Filter (UniformFun.{u_2, u_3} (↑K : Type u_2) α))
⊢ Tendsto (β := UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      (Function.comp (β := X →ᵤ[𝔖] α)
        (Function.comp (β := (↑K : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
            (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
          (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α))
        ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
      ℱ
      (𝓝
        (Function.comp (α := X →ᵤ[𝔖] α) (β := (↑K : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
            (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
          (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α)
          ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f : X →ᵤ[𝔖] α))) ↔
    Tendsto (K.restrict (π := fun (x : X) ↦ α) ∘ F) ℱ (𝓝 (K.restrict (π := fun (x : X) ↦ α) f))

Tactic:
rw [← (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).tendsto_uniformFun_iff_pi]

Premises used: Iff.mpr, equicontinuous_restrict_iff, Equicontinuous.tendsto_uniformFun_iff_pi