-- Mathlib/Topology/UniformSpace/Ascoli.lean
theorem EquicontinuousOn.tendsto_uniformOnFun_iff_pi'
    {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
    (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (ℱ : Filter ι) (f : X → α) :
    Tendsto (UniformOnFun.ofFun 𝔖 ∘ F) ℱ (𝓝 <| UniformOnFun.ofFun 𝔖 f) ↔
    Tendsto ((⋃₀ 𝔖).restrict ∘ F) ℱ (𝓝 <| (⋃₀ 𝔖).restrict f)

Proof state:
case a
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.restrict ∘ F) ℱ (𝓝 (K.restrict f))

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

Result:
case a
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (⇑UniformFun.ofFun ∘ K.restrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.restrict f)))

Proof state:
case a
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.restrict ∘ F) ℱ (𝓝 (K.restrict f))

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)

Result:
case a
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.restrict ∘ F) ℱ (𝓝 (K.restrict f))

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
simp_rw [UniformOnFun.topologicalSpace_eq, Pi.induced_restrict_sUnion 𝔖 (π := fun _ ↦ α),
  _root_.nhds_iInf, nhds_induced, tendsto_iInf, tendsto_comap_iff]

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ (∀ i ∈ 𝔖,
      Tendsto ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
        (𝓝 ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f)))) ↔
    ∀ i ∈ 𝔖, Tendsto (i.restrict ∘ F) ℱ (𝓝 (i.restrict f))

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔
    Tendsto ((⋃₀ 𝔖).restrict ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict f))

Tactic:
rw [← Filter.tendsto_comap_iff (g := (⋃₀ 𝔖).restrict), ← nhds_induced]

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ (∀ i ∈ 𝔖,
      Tendsto ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
        (𝓝 ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f)))) ↔
    ∀ i ∈ 𝔖, Tendsto (i.restrict ∘ F) ℱ (𝓝 (i.restrict f))

Tactic:
congrm ∀ K (hK : K ∈ 𝔖), ?_

Result:
case a
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.restrict ∘ F) ℱ (𝓝 (K.restrict f))

Proof state:
case a
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : 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 ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (⇑UniformFun.ofFun ∘ K.restrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.restrict f)))

Tactic:
rfl

Result:
no goals