Let X and Tx be given.

Assume Hcomp: compact_space X Tx.

Let N be given.

We will prove ∃S x : set, subnet_pack_of_in X N S ∧ net_pack_converges X Tx S x.

Apply HNpack to the current goal.

Let JN be given.

Assume Hexle: ∃leN netN : set, N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN X ∧ functional_graph netN ∧ graph_domain_subset netN JN.

Apply Hexle to the current goal.

Let leN be given.

Assume Hexnet: ∃netN : set, N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN X ∧ functional_graph netN ∧ graph_domain_subset netN JN.

Apply Hexnet to the current goal.

Let netN be given.

Assume Hdata: N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN X ∧ functional_graph netN ∧ graph_domain_subset netN JN.

Apply (and5E (N = net_pack JN leN netN) (directed_set JN leN) (total_function_on netN JN X) (functional_graph netN) (graph_domain_subset netN JN) Hdata) to the current goal.

Assume HN Hdir Htot Hgraph Hdom.

We prove the intermediate claim Hexacc: ∃x0 : set, accumulation_point_of_net_on X Tx (net_pack_fun N) (net_pack_index N) (net_pack_le N) x0.

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

rewrite the current goal using (net_pack_fun_eq JN leN netN) (from left to right).

rewrite the current goal using (net_pack_index_eq JN leN netN) (from left to right).

rewrite the current goal using (net_pack_le_eq JN leN netN) (from left to right).

An exact proof term for the current goal is (compact_space_net_has_accumulation_point_on X Tx netN JN leN Hcomp Hdir Htot Hgraph Hdom).

Apply Hexacc to the current goal.

Let x0 be given.

Assume Hacc_on: accumulation_point_of_net_on X Tx (net_pack_fun N) (net_pack_index N) (net_pack_le N) x0.

We prove the intermediate claim Hexsub: ∃K leK phi sub : set, subnet_of_witness (net_pack_fun N) sub (net_pack_index N) (net_pack_le N) K leK X phi ∧ net_converges_on X Tx sub K leK x0.

An exact proof term for the current goal is (subnet_converges_to_accumulation_witnessed_on X Tx (net_pack_fun N) x0 (net_pack_index N) (net_pack_le N) Hacc_on).

Apply Hexsub to the current goal.

Let K0 be given.

Assume HexleK0: ∃leK0 phi0 sub0 : set, subnet_of_witness (net_pack_fun N) sub0 (net_pack_index N) (net_pack_le N) K0 leK0 X phi0 ∧ net_converges_on X Tx sub0 K0 leK0 x0.

Apply HexleK0 to the current goal.

Let leK0 be given.

Assume Hexphi0: ∃phi0 sub0 : set, subnet_of_witness (net_pack_fun N) sub0 (net_pack_index N) (net_pack_le N) K0 leK0 X phi0 ∧ net_converges_on X Tx sub0 K0 leK0 x0.

Apply Hexphi0 to the current goal.

Let phi0 be given.

Assume Hexsub0: ∃sub0 : set, subnet_of_witness (net_pack_fun N) sub0 (net_pack_index N) (net_pack_le N) K0 leK0 X phi0 ∧ net_converges_on X Tx sub0 K0 leK0 x0.

Apply Hexsub0 to the current goal.

Let sub0 be given.

Assume Hsubconv: subnet_of_witness (net_pack_fun N) sub0 (net_pack_index N) (net_pack_le N) K0 leK0 X phi0 ∧ net_converges_on X Tx sub0 K0 leK0 x0.

We use (net_pack K0 leK0 sub0) to witness the existential quantifier.

We use x0 to witness the existential quantifier.

We will prove subnet_pack_of_in X N (net_pack K0 leK0 sub0) ∧ net_pack_converges X Tx (net_pack K0 leK0 sub0) x0.

Apply andI to the current goal.

We will prove ∃phi0 : set, subnet_of_witness (net_pack_fun N) (net_pack_fun (net_pack K0 leK0 sub0)) (net_pack_index N) (net_pack_le N) (net_pack_index (net_pack K0 leK0 sub0)) (net_pack_le (net_pack K0 leK0 sub0)) X phi0.

We use phi0 to witness the existential quantifier.

rewrite the current goal using (net_pack_fun_eq K0 leK0 sub0) (from left to right).

rewrite the current goal using (net_pack_index_eq K0 leK0 sub0) (from left to right).

rewrite the current goal using (net_pack_le_eq K0 leK0 sub0) (from left to right).

An exact proof term for the current goal is (andEL (subnet_of_witness (net_pack_fun N) sub0 (net_pack_index N) (net_pack_le N) K0 leK0 X phi0) (net_converges_on X Tx sub0 K0 leK0 x0) Hsubconv).

We will prove net_pack_converges X Tx (net_pack K0 leK0 sub0) x0.

We will prove ∃J1 le1 net1 : set, net_pack K0 leK0 sub0 = net_pack J1 le1 net1 ∧ net_converges_on X Tx net1 J1 le1 x0.

We use K0 to witness the existential quantifier.

We use leK0 to witness the existential quantifier.

We use sub0 to witness the existential quantifier.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is (andER (subnet_of_witness (net_pack_fun N) sub0 (net_pack_index N) (net_pack_le N) K0 leK0 X phi0) (net_converges_on X Tx sub0 K0 leK0 x0) Hsubconv).

∎