Set Hcand to be the term Ascoli_g_pointwise_closure X Tx Y dY F.

We use Hcand to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HFsubHcand: F ⊆ Hcand.

We prove the intermediate claim HTy: topology_on Y Ty.

An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).

Set Dom to be the term function_space X Y.

Set Tpt to be the term pointwise_convergence_topology X Tx Y Ty.

We prove the intermediate claim HTpt: topology_on Dom Tpt.

An exact proof term for the current goal is (pointwise_convergence_topology_is_topology X Tx Y Ty HTx HTy).

We prove the intermediate claim HFsubDom: F ⊆ Dom.

Let f0 be given.

Assume Hf0F: f0 ∈ F.

We prove the intermediate claim Hf0C: f0 ∈ CXY.

An exact proof term for the current goal is (HFcont f0 Hf0F).

An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f0 Hf0C).

An exact proof term for the current goal is (subset_of_closure Dom Tpt F HTpt HFsubDom).

An exact proof term for the current goal is HFsubHcand.

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_set_sub_CXY X Tx Y dY F HTx HdY HFcont Hequi).

Set Thcand to be the term subspace_topology CXY Tcc Hcand.

We prove the intermediate claim HTcc: topology_on CXY Tcc.

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

We prove the intermediate claim HHcandSubCXY: Hcand ⊆ CXY.

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_set_sub_CXY X Tx Y dY F HTx HdY HFcont Hequi).

We prove the intermediate claim HThcand: topology_on Hcand Thcand.

An exact proof term for the current goal is (subspace_topology_is_topology CXY Tcc Hcand HTcc HHcandSubCXY).

We prove the intermediate claim HThcandEq: Thcand = subspace_topology (continuous_function_space X Tx Y (metric_topology Y dY)) (compact_convergence_topology_metric_C X Tx Y dY) Hcand.

Use reflexivity.

We prove the intermediate claim HHcandDef: Hcand = Ascoli_g_pointwise_closure X Tx Y dY F.

Use reflexivity.

Apply (compact_space_of_every_net_pack_has_convergent_subnet_pack Hcand Thcand HThcand) to the current goal.

Let N be given.

Assume HN: net_pack_in_space Hcand N.

We will prove ∃S x : set, subnet_pack_of_in Hcand N S ∧ net_pack_converges Hcand Thcand S x.

Apply HN to the current goal.

Let J be given.

Assume Hexle: ∃le net : set, N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J Hcand ∧ functional_graph net ∧ graph_domain_subset net J.

Apply Hexle to the current goal.

Let le be given.

Assume Hexnet: ∃net : set, N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J Hcand ∧ functional_graph net ∧ graph_domain_subset net J.

Apply Hexnet to the current goal.

Let net be given.

Assume HNpack: N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J Hcand ∧ functional_graph net ∧ graph_domain_subset net J.

We prove the intermediate claim HNdef: N = net_pack J le net.

Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J Hcand) (functional_graph net) (graph_domain_subset net J) HNpack (N = net_pack J le net)) to the current goal.

Assume H1 H2 H3 H4 H5.

An exact proof term for the current goal is H1.

We prove the intermediate claim Hdir: directed_set J le.

Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J Hcand) (functional_graph net) (graph_domain_subset net J) HNpack (directed_set J le)) to the current goal.

Assume H1 H2 H3 H4 H5.

An exact proof term for the current goal is H2.

We prove the intermediate claim Htot: total_function_on net J Hcand.

Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J Hcand) (functional_graph net) (graph_domain_subset net J) HNpack (total_function_on net J Hcand)) to the current goal.

Assume H1 H2 H3 H4 H5.

An exact proof term for the current goal is H3.

We prove the intermediate claim Hgraph: functional_graph net.

Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J Hcand) (functional_graph net) (graph_domain_subset net J) HNpack (functional_graph net)) to the current goal.

Assume H1 H2 H3 H4 H5.

An exact proof term for the current goal is H4.

We prove the intermediate claim Hdom: graph_domain_subset net J.

Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J Hcand) (functional_graph net) (graph_domain_subset net J) HNpack (graph_domain_subset net J)) to the current goal.

Assume H1 H2 H3 H4 H5.

An exact proof term for the current goal is H5.

We prove the intermediate claim HTy: topology_on Y Ty.

An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).

We prove the intermediate claim Hcoord: ∀a : set, a ∈ X → ∃Ni Si x : set, net_pack_in_space (closure_of Y Ty (Ascoli_F_at X Y a F)) Ni ∧ Ni = net_pack J le (graph J (λj : set ⇒ apply_fun (apply_fun net j) a)) ∧ subnet_pack_of_in (closure_of Y Ty (Ascoli_F_at X Y a F)) Ni Si ∧ net_pack_converges (closure_of Y Ty (Ascoli_F_at X Y a F)) (subspace_topology Y Ty (closure_of Y Ty (Ascoli_F_at X Y a F))) Si x.

Let a be given.

Assume HaX: a ∈ X.

Set Ka to be the term closure_of Y Ty (Ascoli_F_at X Y a F).

Set TKa to be the term subspace_topology Y Ty Ka.

Set neta to be the term graph J (λj : set ⇒ apply_fun (apply_fun net j) a).

Set Ni to be the term net_pack J le neta.

We use Ni to witness the existential quantifier.

We prove the intermediate claim HNiIn: net_pack_in_space Ka Ni.

We will prove ∃J0 le0 net0 : set, Ni = net_pack J0 le0 net0 ∧ directed_set J0 le0 ∧ total_function_on net0 J0 Ka ∧ functional_graph net0 ∧ graph_domain_subset net0 J0.

We use J to witness the existential quantifier.

We use le to witness the existential quantifier.

We use neta to witness the existential quantifier.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Hdir.

Apply (total_function_on_graph J Ka (λj : set ⇒ apply_fun (apply_fun net j) a)) to the current goal.

Let j be given.

Assume HjJ: j ∈ J.

We prove the intermediate claim HfjH: apply_fun net j ∈ Hcand.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y net J Hcand j Htot HjJ).

We prove the intermediate claim HfjG: apply_fun net j ∈ Ascoli_g_pointwise_closure X Tx Y dY F.

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

An exact proof term for the current goal is HfjH.

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_coord X Tx Y dY F (apply_fun net j) a HTx HdY HFcont HfjG HaX).

An exact proof term for the current goal is (functional_graph_graph J (λj : set ⇒ apply_fun (apply_fun net j) a)).

An exact proof term for the current goal is (graph_domain_subset_graph J (λj : set ⇒ apply_fun (apply_fun net j) a)).

We prove the intermediate claim HKaComp: compact_space Ka TKa.

An exact proof term for the current goal is (Hpwc a HaX).

We prove the intermediate claim HexSub: ∃Si x : set, subnet_pack_of_in Ka Ni Si ∧ net_pack_converges Ka TKa Si x.

An exact proof term for the current goal is (compact_space_implies_every_net_pack_has_convergent_subnet_pack Ka TKa HKaComp Ni HNiIn).

Apply HexSub to the current goal.

Let Si be given.

Assume Hexx: ∃x : set, subnet_pack_of_in Ka Ni Si ∧ net_pack_converges Ka TKa Si x.

Apply Hexx to the current goal.

Let x be given.

Assume Hsubconv: subnet_pack_of_in Ka Ni Si ∧ net_pack_converges Ka TKa Si x.

We use Si to witness the existential quantifier.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HNiIn.

Use reflexivity.

An exact proof term for the current goal is (andEL (subnet_pack_of_in Ka Ni Si) (net_pack_converges Ka TKa Si x) Hsubconv).

An exact proof term for the current goal is (andER (subnet_pack_of_in Ka Ni Si) (net_pack_converges Ka TKa Si x) Hsubconv).

An exact proof term for the current goal is (Ascoli_theorem_47_1a_diag_upgrade X Tx Y dY F Hcand Thcand N J le net HTx HdY HHcandSubCXY HHcandDef HThcandEq HThcand HFcont Hequi Hpwc HNdef Hdir Htot Hgraph Hdom Hcoord).