Set Ty to be the term metric_topology Y dY.

Set CXY to be the term continuous_function_space X Tx Y Ty.

Set Tco to be the term compact_open_topology_C X Tx Y Ty.

We prove the intermediate claim HFsubCXY: F ⊆ CXY.

An exact proof term for the current goal is HFcont.

We prove the intermediate claim HexH: ∃H0 : set, F ⊆ H0 ∧ H0 ⊆ CXY ∧ compact_space H0 (subspace_topology CXY (compact_convergence_topology_metric_C X Tx Y dY) H0).

An exact proof term for the current goal is (andER (F ⊆ CXY) (∃H0 : set, F ⊆ H0 ∧ H0 ⊆ CXY ∧ compact_space H0 (subspace_topology CXY (compact_convergence_topology_metric_C X Tx Y dY) H0)) Hrel).

Apply HexH to the current goal.

Let H0 be given.

Assume H0pack.

We prove the intermediate claim H0mid: F ⊆ H0 ∧ H0 ⊆ CXY.

An exact proof term for the current goal is (andEL (F ⊆ H0 ∧ H0 ⊆ CXY) (compact_space H0 (subspace_topology CXY (compact_convergence_topology_metric_C X Tx Y dY) H0)) H0pack).

We prove the intermediate claim HFsubH0: F ⊆ H0.

An exact proof term for the current goal is (andEL (F ⊆ H0) (H0 ⊆ CXY) H0mid).

We prove the intermediate claim HH0sub: H0 ⊆ CXY.

An exact proof term for the current goal is (andER (F ⊆ H0) (H0 ⊆ CXY) H0mid).

We prove the intermediate claim H0comp_cc: compact_space H0 (subspace_topology CXY (compact_convergence_topology_metric_C X Tx Y dY) H0).

An exact proof term for the current goal is (andER (F ⊆ H0 ∧ H0 ⊆ CXY) (compact_space H0 (subspace_topology CXY (compact_convergence_topology_metric_C X Tx Y dY) H0)) H0pack).

We prove the intermediate claim HeqTop: compact_open_topology_C X Tx Y Ty = compact_convergence_topology_metric_C X Tx Y dY.

An exact proof term for the current goal is (compact_open_eq_compact_convergence_on_C X Tx Y dY HTx HdY).

We prove the intermediate claim HeqTop': (compact_convergence_topology_metric_C X Tx Y dY) = Tco.

rewrite the current goal using HeqTop (from right to left).

Use reflexivity.

We prove the intermediate claim HsubEq: subspace_topology CXY (compact_convergence_topology_metric_C X Tx Y dY) H0 = subspace_topology CXY Tco H0.

An exact proof term for the current goal is (subspace_topology_eq_of_eq CXY (compact_convergence_topology_metric_C X Tx Y dY) Tco H0 HeqTop').

We prove the intermediate claim H0comp_co: compact_space H0 (subspace_topology CXY Tco H0).

rewrite the current goal using HsubEq (from right to left).

An exact proof term for the current goal is H0comp_cc.

We prove the intermediate claim HequiH0: equicontinuous_family X Tx Y dY H0.

An exact proof term for the current goal is (compact_subspace_CXY_equicontinuous X Tx Y dY H0 HTx HdY Hlc HHx HH0sub H0comp_co).

We prove the intermediate claim HequiH0_core: topology_on X Tx ∧ metric_on Y dY ∧ H0 ⊆ CXY ∧ ∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ ∀f : set, f ∈ H0 → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps.

An exact proof term for the current goal is HequiH0.

We will prove topology_on X Tx ∧ metric_on Y dY ∧ F ⊆ continuous_function_space X Tx Y (metric_topology Y dY) ∧ ∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ ∀f : set, f ∈ F → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HdY.

An exact proof term for the current goal is HFsubCXY.

Let x0 be given.

Assume Hx0X: x0 ∈ X.

Let eps be given.

Assume Heps: eps ∈ R ∧ Rlt 0 eps.

We prove the intermediate claim HforallH0: ∀x1 : set, x1 ∈ X → ∀e1 : set, e1 ∈ R ∧ Rlt 0 e1 → ∃U : set, U ∈ Tx ∧ x1 ∈ U ∧ ∀f : set, f ∈ H0 → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x1)) e1.

An exact proof term for the current goal is (andER ((topology_on X Tx ∧ metric_on Y dY) ∧ H0 ⊆ CXY) (∀x1 : set, x1 ∈ X → ∀e1 : set, e1 ∈ R ∧ Rlt 0 e1 → ∃U : set, U ∈ Tx ∧ x1 ∈ U ∧ ∀f : set, f ∈ H0 → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x1)) e1) HequiH0_core).

We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ ∀f : set, f ∈ H0 → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps.

An exact proof term for the current goal is (HforallH0 x0 Hx0X eps Heps).

Apply HexU to the current goal.

Let U be given.

Assume HU.

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x0 ∈ U) (∀f : set, f ∈ H0 → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps) HU).

Let f be given.

Assume HfF: f ∈ F.

Let x be given.

Assume HxX: x ∈ X.

Assume HxU: x ∈ U.

We prove the intermediate claim HfH0: f ∈ H0.

An exact proof term for the current goal is (HFsubH0 f HfF).

We prove the intermediate claim HUprop: ∀f0 : set, f0 ∈ H0 → ∀x1 : set, x1 ∈ X → x1 ∈ U → Rlt (apply_fun dY (apply_fun f0 x1,apply_fun f0 x0)) eps.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x0 ∈ U) (∀f0 : set, f0 ∈ H0 → ∀x1 : set, x1 ∈ X → x1 ∈ U → Rlt (apply_fun dY (apply_fun f0 x1,apply_fun f0 x0)) eps) HU).

An exact proof term for the current goal is (HUprop f HfH0 x HxX HxU).