-- Mathlib/Topology/UniformSpace/Ascoli.lean
theorem EquicontinuousOn.isClosed_range_pi_of_uniformOnFun'
    {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
    (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K)
    (H : IsClosed (range <| UniformOnFun.ofFun 𝔖 ∘ F)) :
    IsClosed (range <| (⋃₀ 𝔖).restrict ∘ F)

Proof state:
case inr
ι : 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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : Nonempty α
⊢ ∀ (x : X → α),
    (∃ U, ↑U ≤ ⊤ ∧ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (↑U) (𝓝 ((UniformOnFun.ofFun 𝔖) x))) →
      (⋃₀ 𝔖).restrict x ∈ (⋃₀ 𝔖).restrict '' range F

Tactic:
exact fun f ⟨u, _, hu⟩ ↦ mem_image_of_mem _ <| H.mem_of_tendsto hu <|
  Eventually.of_forall mem_range_self

Result:
no goals

Proof state:
case inr
ι : 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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : Nonempty α
⊢ IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))

Tactic:
simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
  mapClusterPt_iff_ultrafilter, range_comp, Subtype.coe_injective.surjective_comp_right.forall,
  ← restrict_eq, ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi' 𝔖_compact F_eqcont]

Result:
case inr
ι : 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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : Nonempty α
⊢ ∀ (x : X → α),
    (∃ U, ↑U ≤ ⊤ ∧ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (↑U) (𝓝 ((UniformOnFun.ofFun 𝔖) x))) →
      (⋃₀ 𝔖).restrict x ∈ (⋃₀ 𝔖).restrict '' range F

Proof state:
case inl
ι : 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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : IsEmpty α
⊢ IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))

Tactic:
simp [isClosed_discrete]

Result:
no goals

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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
⊢ IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))

Tactic:
rcases isEmpty_or_nonempty α with _ | _

Result:
case inl
ι : 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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : IsEmpty α
⊢ IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))

case inr
ι : 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
H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : Nonempty α
⊢ IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))