-- Mathlib/Topology/UniformSpace/Ascoli.lean
theorem ArzelaAscoli.isCompact_of_equicontinuous
    (S : Set C(X, α)) (hS1 : IsCompact (ContinuousMap.toFun '' S))
    (hS2 : Equicontinuous ((↑) : S → X → α)) : IsCompact S

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
h : IsInducing ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)
⊢ IsCompact S

Tactic:
rw [isCompact_iff_compactSpace] at hS1 ⊢

Result:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : CompactSpace ↑(ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
h : IsInducing ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)
⊢ CompactSpace ↑S

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ IsInducing ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)

Tactic:
rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]

Result:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.47463) ∘ Subtype.val ∘ ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯))

X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ Set (Set X)

X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ ⋃₀ ?m.47463 = univ

X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ ∀ K ∈ ?m.47463, IsCompact K

X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ ∀ K ∈ ?m.47463, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)) K

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.47463) ∘ Subtype.val ∘ ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯))

Tactic:
exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal

Result:
no goals

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ ∀ K ∈ {K | IsCompact K}, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)) K

Tactic:
exact fun K _ ↦ hS2.equicontinuousOn K

Result:
no goals

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ ⋃₀ {K | IsCompact K} = univ

Tactic:
exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton)

Result:
no goals

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ IsCompact S

Tactic:
suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective) by
  rw [isCompact_iff_compactSpace] at hS1 ⊢
  exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace

Result:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ IsInducing ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
⊢ ∀ K ∈ {K | IsCompact K}, IsCompact K

Tactic:
exact fun _ ↦ id

Result:
no goals

Proof state:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : CompactSpace ↑(ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x => ⇑↑x
h : IsInducing ⇑(Equiv.Set.image (fun f => ⇑f) S ⋯)
⊢ CompactSpace ↑S

Tactic:
exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace

Result:
no goals