Let I, Xi and N be given.
Assume HIne: I ≠ Empty.
Assume HN: net_pack_in_space (product_space I Xi) N.
Assume Hcoord: ∀i : set, i ∈ I → ∃Ni Si x : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x.
Set Pi to be the term (λi : set ⇒ λx : set ⇒ ∃Ni Si : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x).
Set x to be the term graph I (λi : set ⇒ Eps_i (Pi i)).
We prove the intermediate claim HxX: x ∈ product_space I Xi.
Apply (product_space_graphI I Xi (λi0 : set ⇒ Eps_i (Pi i0))) to the current goal.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hex: ∃y : set, Pi i y.
Apply (Hcoord i HiI) to the current goal.
Let Ni be given.
Assume HexSi: ∃Si x0 : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
Apply HexSi to the current goal.
Let Si be given.
Assume Hexx: ∃x0 : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
Apply Hexx to the current goal.
Let x0 be given.
Assume Hpack: net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
We use x0 to witness the existential quantifier.
We prove the intermediate claim HPiDef: Pi i x0 = ∃Ni0 Si0 : set, net_pack_in_space (space_family_set Xi i) Ni0 ∧ net_pack_index Ni0 = net_pack_index N ∧ net_pack_le Ni0 = net_pack_le N ∧ Ni0 = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni0 Si0 ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si0 x0.
Use reflexivity.
rewrite the current goal using HPiDef (from left to right).
We use Ni to witness the existential quantifier.
We use Si to witness the existential quantifier.
An exact proof term for the current goal is Hpack.
We prove the intermediate claim HPi: Pi i (Eps_i (Pi i)).
An exact proof term for the current goal is (Eps_i_ex (Pi i) Hex).
Apply HPi to the current goal.
Let Ni be given.
Assume HexSi: ∃Si : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
Apply HexSi to the current goal.
Let Si be given.
Assume HSi: net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
We prove the intermediate claim Hconv: net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
An exact proof term for the current goal is (andER (net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi).
An exact proof term for the current goal is (net_pack_converges_implies_x_in_space (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)) Hconv).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hex: ∃y : set, Pi i y.
Apply (Hcoord i HiI) to the current goal.
Let Ni be given.
Assume HexSi: ∃Si x0 : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
Apply HexSi to the current goal.
Let Si be given.
Assume Hexx: ∃x0 : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
Apply Hexx to the current goal.
Let x0 be given.
Assume Hpack: net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
We use x0 to witness the existential quantifier.
We prove the intermediate claim HPiDef: Pi i x0 = ∃Ni0 Si0 : set, net_pack_in_space (space_family_set Xi i) Ni0 ∧ net_pack_index Ni0 = net_pack_index N ∧ net_pack_le Ni0 = net_pack_le N ∧ Ni0 = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni0 Si0 ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si0 x0.
Use reflexivity.
rewrite the current goal using HPiDef (from left to right).
We use Ni to witness the existential quantifier.
We use Si to witness the existential quantifier.
An exact proof term for the current goal is Hpack.
We prove the intermediate claim HPi: Pi i (Eps_i (Pi i)).
An exact proof term for the current goal is (Eps_i_ex (Pi i) Hex).
Apply HPi to the current goal.
Let Ni be given.
Assume HexSi: ∃Si : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
Apply HexSi to the current goal.
Let Si be given.
Assume HSi: net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
We prove the intermediate claim Hconv: net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
An exact proof term for the current goal is (andER (net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi).
An exact proof term for the current goal is (net_pack_converges_implies_topology_on (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)) Hconv).
Set FinI to be the term finite_subcollections I.
Set leFin to be the term inclusion_rel FinI.
We prove the intermediate claim HdirFin: directed_set FinI leFin.
An exact proof term for the current goal is (finite_subcollections_directed_by_inclusion_rel I).
We prove the intermediate claim Hcoord_x: ∀i : set, i ∈ I → ∃Ni Si : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (apply_fun x i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hex: ∃y : set, Pi i y.
Apply (Hcoord i HiI) to the current goal.
Let Ni be given.
Assume HexSi: ∃Si x0 : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
Apply HexSi to the current goal.
Let Si be given.
Assume Hexx: ∃x0 : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
Apply Hexx to the current goal.
Let x0 be given.
Assume Hpack: net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si x0.
We use x0 to witness the existential quantifier.
We prove the intermediate claim HPiDef: Pi i x0 = ∃Ni0 Si0 : set, net_pack_in_space (space_family_set Xi i) Ni0 ∧ net_pack_index Ni0 = net_pack_index N ∧ net_pack_le Ni0 = net_pack_le N ∧ Ni0 = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj0 : set ⇒ apply_fun (apply_fun (net_pack_fun N) j0) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni0 Si0 ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si0 x0.
Use reflexivity.
rewrite the current goal using HPiDef (from left to right).
We use Ni to witness the existential quantifier.
We use Si to witness the existential quantifier.
An exact proof term for the current goal is Hpack.
We prove the intermediate claim HPi: Pi i (Eps_i (Pi i)).
An exact proof term for the current goal is (Eps_i_ex (Pi i) Hex).
Apply HPi to the current goal.
Let Ni be given.
Assume HexSi: ∃Si : set, net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
Apply HexSi to the current goal.
Let Si be given.
Assume HSi: net_pack_in_space (space_family_set Xi i) Ni ∧ net_pack_index Ni = net_pack_index N ∧ net_pack_le Ni = net_pack_le N ∧ Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)) ∧ subnet_pack_of_in (space_family_set Xi i) Ni Si ∧ net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)).
We use Ni to witness the existential quantifier.
We use Si to witness the existential quantifier.
Apply (and6I (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (apply_fun x i))) to the current goal.
Apply (and6E (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi (net_pack_in_space (space_family_set Xi i) Ni)) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H1.
Apply (and6E (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi (net_pack_index Ni = net_pack_index N)) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H2.
Apply (and6E (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi (net_pack_le Ni = net_pack_le N)) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H3.
Apply (and6E (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i)))) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H4.
Apply (and6E (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi (subnet_pack_of_in (space_family_set Xi i) Ni Si)) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H5.
We prove the intermediate claim Hxdef: x = graph I (λi0 : set ⇒ Eps_i (Pi i0)).
Use reflexivity.
We prove the intermediate claim Hxval: apply_fun x i = Eps_i (Pi i).
rewrite the current goal using Hxdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph I (λi0 : set ⇒ Eps_i (Pi i0)) i HiI).
rewrite the current goal using Hxval (from left to right) at position 1.
Apply (and6E (net_pack_in_space (space_family_set Xi i) Ni) (net_pack_index Ni = net_pack_index N) (net_pack_le Ni = net_pack_le N) (Ni = net_pack (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) i))) (subnet_pack_of_in (space_family_set Xi i) Ni Si) (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i))) HSi (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (Eps_i (Pi i)))) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H6.
We prove the intermediate claim HexS: ∃J le net : set, subnet_pack_of_in (product_space I Xi) N (net_pack J le net) ∧ (∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun J net (product_eval_map I Xi i)) J le (apply_fun x i)).
An exact proof term for the current goal is (Tychonoff_coordinate_subnets_to_common_subnet I Xi N x HIne HN HxX Hcoord_x).
Apply HexS to the current goal.
Let J be given.
Assume Hexle: ∃le net : set, subnet_pack_of_in (product_space I Xi) N (net_pack J le net) ∧ (∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun J net (product_eval_map I Xi i)) J le (apply_fun x i)).
Apply Hexle to the current goal.
Let le be given.
Assume Hexnet: ∃net : set, subnet_pack_of_in (product_space I Xi) N (net_pack J le net) ∧ (∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun J net (product_eval_map I Xi i)) J le (apply_fun x i)).
Apply Hexnet to the current goal.
Let net be given.
Assume HScoord.
We prove the intermediate claim HSsub: subnet_pack_of_in (product_space I Xi) N (net_pack J le net).
An exact proof term for the current goal is (andEL (subnet_pack_of_in (product_space I Xi) N (net_pack J le net)) (∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun J net (product_eval_map I Xi i)) J le (apply_fun x i)) HScoord).
We prove the intermediate claim Hallcoord: ∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun J net (product_eval_map I Xi i)) J le (apply_fun x i).
An exact proof term for the current goal is (andER (subnet_pack_of_in (product_space I Xi) N (net_pack J le net)) (∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun J net (product_eval_map I Xi i)) J le (apply_fun x i)) HScoord).
We prove the intermediate claim HS_w: ∃phi : set, subnet_of_witness (net_pack_fun N) (net_pack_fun (net_pack J le net)) (net_pack_index N) (net_pack_le N) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) (product_space I Xi) phi.
An exact proof term for the current goal is HSsub.
Apply HS_w to the current goal.
Let phi be given.
Assume Hw.
We prove the intermediate claim HdirS: directed_set (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)).
An exact proof term for the current goal is (subnet_of_witness_dirK (net_pack_fun N) (net_pack_fun (net_pack J le net)) (net_pack_index N) (net_pack_le N) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) (product_space I Xi) phi Hw).
We prove the intermediate claim Htots: total_function_on (net_pack_fun (net_pack J le net)) (net_pack_index (net_pack J le net)) (product_space I Xi).
An exact proof term for the current goal is (subnet_of_witness_totsub (net_pack_fun N) (net_pack_fun (net_pack J le net)) (net_pack_index N) (net_pack_le N) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) (product_space I Xi) phi Hw).
We prove the intermediate claim Hgs: functional_graph (net_pack_fun (net_pack J le net)).
An exact proof term for the current goal is (subnet_of_witness_graphsub (net_pack_fun N) (net_pack_fun (net_pack J le net)) (net_pack_index N) (net_pack_le N) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) (product_space I Xi) phi Hw).
We prove the intermediate claim Hds: graph_domain_subset (net_pack_fun (net_pack J le net)) (net_pack_index (net_pack J le net)).
An exact proof term for the current goal is (subnet_of_witness_domsub (net_pack_fun N) (net_pack_fun (net_pack J le net)) (net_pack_index N) (net_pack_le N) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) (product_space I Xi) phi Hw).
We prove the intermediate claim Hallcoord0: ∀i : set, i ∈ I → net_converges_on (space_family_set Xi i) (space_family_topology Xi i) (compose_fun (net_pack_index (net_pack J le net)) (net_pack_fun (net_pack J le net)) (product_eval_map I Xi i)) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) (apply_fun x i).
Let i be given.
Assume HiI: i ∈ I.
rewrite the current goal using (net_pack_index_eq J le net) (from left to right).
rewrite the current goal using (net_pack_le_eq J le net) (from left to right).
rewrite the current goal using (net_pack_fun_eq J le net) (from left to right).
An exact proof term for the current goal is (Hallcoord i HiI).
We use (net_pack J le net) 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 HSsub.
We will prove net_pack_converges (product_space I Xi) (product_topology_full I Xi) (net_pack J le net) x.
We will prove ∃J0 le0 net0 : set, (net_pack J le net) = net_pack J0 le0 net0 ∧ net_converges_on (product_space I Xi) (product_topology_full I Xi) net0 J0 le0 x.
We use (net_pack_index (net_pack J le net)) to witness the existential quantifier.
We use (net_pack_le (net_pack J le net)) to witness the existential quantifier.
We use (net_pack_fun (net_pack J le net)) to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using (net_pack_index_eq J le net) (from left to right).
rewrite the current goal using (net_pack_le_eq J le net) (from left to right).
rewrite the current goal using (net_pack_fun_eq J le net) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (net_converges_on_product_topology_full_of_all_coord_converge I Xi (net_pack_fun (net_pack J le net)) (net_pack_index (net_pack J le net)) (net_pack_le (net_pack J le net)) x HIne HcompTop HdirS Htots Hgs Hds HxX Hallcoord0).
∎