Let I, Xi, N and x be given.
Assume HIne: I ≠ Empty.
Assume HN: net_pack_in_space (product_space I Xi) N.
Assume HxX: x ∈ product_space I Xi.
Assume Hcoord: ∀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).
We will prove ∃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)).
We prove the intermediate claim Hxcoord: ∀i : set, i ∈ I → apply_fun x i ∈ space_family_set Xi i.
Let i be given.
Assume HiI: i ∈ I.
Apply (Hcoord i HiI) 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 (apply_fun x i).
Apply HexSi to the current goal.
Let Si 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 (apply_fun x i).
We prove the intermediate claim Hconv: net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (apply_fun x i).
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 (apply_fun x i)) Hpack (net_pack_converges (space_family_set Xi i) (space_family_topology Xi i) Si (apply_fun x i))) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H6.
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 (apply_fun x i) Hconv).
We prove the intermediate claim HexW: ∃W : set, well_ordered_set W ∧ equip I W.
An exact proof term for the current goal is (well_ordering_theorem_equip I).
Apply HexW to the current goal.
Let W be given.
Assume HWpack: well_ordered_set W ∧ equip I W.
We prove the intermediate claim HWwo: well_ordered_set W.
An exact proof term for the current goal is (andEL (well_ordered_set W) (equip I W) HWpack).
We prove the intermediate claim HWequip: equip I W.
An exact proof term for the current goal is (andER (well_ordered_set W) (equip I W) HWpack).
Apply HWequip to the current goal.
Let idx be given.
Assume Hbij: bij I W idx.
We prove the intermediate claim HidxMap: ∀i : set, i ∈ I → idx i ∈ W.
Apply (bijE I W idx Hbij (∀i : set, i ∈ I → idx i ∈ W)) to the current goal.
Assume _Hmap _Hinj _Hsurj.
An exact proof term for the current goal is _Hmap.
We prove the intermediate claim HidxInj: ∀i j : set, i ∈ I → j ∈ I → idx i = idx j → i = j.
Apply (bijE I W idx Hbij (∀i j : set, i ∈ I → j ∈ I → idx i = idx j → i = j)) to the current goal.
Assume _Hmap _Hinj _Hsurj.
Let i be given.
Let j be given.
Assume HiI: i ∈ I.
Assume HjI: j ∈ I.
Assume Heq: idx i = idx j.
An exact proof term for the current goal is (_Hinj i HiI j HjI Heq).
We prove the intermediate claim HidxSurj: ∀w : set, w ∈ W → ∃i : set, i ∈ I ∧ idx i = w.
Apply (bijE I W idx Hbij (∀w : set, w ∈ W → ∃i : set, i ∈ I ∧ idx i = w)) to the current goal.
Assume _Hmap _Hinj _Hsurj.
An exact proof term for the current goal is _Hsurj.
Set pickI to be the term λw : set ⇒ Eps_i (λi : set ⇒ i ∈ I ∧ idx i = w).
We prove the intermediate claim HpickI: ∀w : set, w ∈ W → pickI w ∈ I ∧ idx (pickI w) = w.
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ idx i = w.
An exact proof term for the current goal is (HidxSurj w HwW).
Apply Hexi to the current goal.
Let i be given.
Assume Hi: i ∈ I ∧ idx i = w.
An exact proof term for the current goal is (Eps_i_ax (λi0 : set ⇒ i0 ∈ I ∧ idx i0 = w) i Hi).
We prove the intermediate claim HpickI_idx: ∀i : set, i ∈ I → pickI (idx i) = i.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HwiW: idx i ∈ W.
An exact proof term for the current goal is (HidxMap i HiI).
We prove the intermediate claim Hpi: pickI (idx i) ∈ I ∧ idx (pickI (idx i)) = idx i.
An exact proof term for the current goal is (HpickI (idx i) HwiW).
We prove the intermediate claim HpiI: pickI (idx i) ∈ I.
An exact proof term for the current goal is (andEL (pickI (idx i) ∈ I) (idx (pickI (idx i)) = idx i) Hpi).
We prove the intermediate claim Heqidx: idx (pickI (idx i)) = idx i.
An exact proof term for the current goal is (andER (pickI (idx i) ∈ I) (idx (pickI (idx i)) = idx i) Hpi).
An exact proof term for the current goal is (HidxInj (pickI (idx i)) i HpiI HiI Heqidx).
We prove the intermediate claim HcoordW: ∀w : set, w ∈ W → ∃Ni Si : set, net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w))) ∧ subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si ∧ net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w)).
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hiw: pickI w ∈ I.
An exact proof term for the current goal is (andEL (pickI w ∈ I) (idx (pickI w) = w) (HpickI w HwW)).
An exact proof term for the current goal is (Hcoord (pickI w) Hiw).
We prove the intermediate claim HNrepr: ∃JN leN netN : set, N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN (product_space I Xi) ∧ functional_graph netN ∧ graph_domain_subset netN JN.
An exact proof term for the current goal is HN.
Apply HNrepr to the current goal.
Let JN be given.
Assume HexleN: ∃leN netN : set, N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN (product_space I Xi) ∧ functional_graph netN ∧ graph_domain_subset netN JN.
Apply HexleN to the current goal.
Let leN be given.
Assume HexnetN: ∃netN : set, N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN (product_space I Xi) ∧ functional_graph netN ∧ graph_domain_subset netN JN.
Apply HexnetN to the current goal.
Let netN be given.
Assume HNdata: N = net_pack JN leN netN ∧ directed_set JN leN ∧ total_function_on netN JN (product_space I Xi) ∧ 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 (product_space I Xi)) (functional_graph netN) (graph_domain_subset netN JN) HNdata) to the current goal.
Assume HNdef HNdir HNtot HNgraph HNdom.
We prove the intermediate claim HNidx: net_pack_index N = JN.
rewrite the current goal using HNdef (from left to right).
An exact proof term for the current goal is (net_pack_index_eq JN leN netN).
We prove the intermediate claim HNle: net_pack_le N = leN.
rewrite the current goal using HNdef (from left to right).
An exact proof term for the current goal is (net_pack_le_eq JN leN netN).
We prove the intermediate claim HNfun: net_pack_fun N = netN.
rewrite the current goal using HNdef (from left to right).
An exact proof term for the current goal is (net_pack_fun_eq JN leN netN).
We prove the intermediate claim HliftWsub: ∀w : set, w ∈ W → ∃Sw : set, subnet_pack_of_in (product_space I Xi) N Sw ∧ net_converges_on (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) (compose_fun (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w))) (net_pack_index Sw) (net_pack_le Sw) (apply_fun x (pickI w)).
Let w be given.
Assume HwW: w ∈ W.
Apply (HcoordW w HwW) to the current goal.
Let Ni be given.
Assume HexSi: ∃Si : set, net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w))) ∧ subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si ∧ net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w)).
Apply HexSi to the current goal.
Let Si be given.
Assume Hpack: net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w))) ∧ subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si ∧ net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w)).
We prove the intermediate claim HsubNiSi: subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si.
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si)) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H5.
Apply HsubNiSi to the current goal.
Let phi be given.
Assume Hwphi: subnet_of_witness (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) (net_pack_index Si) (net_pack_le Si) (space_family_set Xi (pickI w)) phi.
Set K to be the term net_pack_index Si.
Set leK to be the term net_pack_le Si.
Set netSw to be the term compose_fun K phi (net_pack_fun N).
Set Sw to be the term net_pack K leK netSw.
We use Sw to witness the existential quantifier.
Apply andI to the current goal.
We will prove subnet_pack_of_in (product_space I Xi) N Sw.
We prove the intermediate claim HsubDef: subnet_pack_of_in (product_space I Xi) N Sw = ∃phi0 : set, subnet_of_witness (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi0.
Use reflexivity.
rewrite the current goal using HsubDef (from left to right).
We use phi to witness the existential quantifier.
We prove the intermediate claim HtotN0: total_function_on (net_pack_fun N) (net_pack_index N) (product_space I Xi).
rewrite the current goal using HNfun (from left to right).
rewrite the current goal using HNidx (from left to right).
An exact proof term for the current goal is HNtot.
We prove the intermediate claim HgraphN0: functional_graph (net_pack_fun N).
rewrite the current goal using HNfun (from left to right).
An exact proof term for the current goal is HNgraph.
We prove the intermediate claim HdomN0: graph_domain_subset (net_pack_fun N) (net_pack_index N).
rewrite the current goal using HNfun (from left to right).
rewrite the current goal using HNidx (from left to right).
An exact proof term for the current goal is HNdom.
We prove the intermediate claim HdirN0: directed_set (net_pack_index N) (net_pack_le N).
rewrite the current goal using HNidx (from left to right).
rewrite the current goal using HNle (from left to right).
An exact proof term for the current goal is HNdir.
We prove the intermediate claim HNiidx: net_pack_index Ni = net_pack_index N.
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (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.
We prove the intermediate claim HNile: net_pack_le Ni = net_pack_le N.
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (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.
We prove the intermediate claim HdirK: directed_set K leK.
An exact proof term for the current goal is (subnet_of_witness_dirK (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
We prove the intermediate claim Htotphi0: total_function_on phi K (net_pack_index N).
We prove the intermediate claim Htotphi: total_function_on phi K (net_pack_index Ni).
An exact proof term for the current goal is (subnet_of_witness_totphi (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
rewrite the current goal using HNiidx (from right to left).
An exact proof term for the current goal is Htotphi.
We prove the intermediate claim Hgraphphi0: functional_graph phi.
An exact proof term for the current goal is (subnet_of_witness_graphphi (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
We prove the intermediate claim Hdomphi0: graph_domain_subset phi K.
An exact proof term for the current goal is (subnet_of_witness_domphi (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
We prove the intermediate claim Hmono0: ∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ (net_pack_le N).
We prove the intermediate claim Hmono: ∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ (net_pack_le Ni).
An exact proof term for the current goal is (subnet_of_witness_mono (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
rewrite the current goal using HNile (from right to left).
An exact proof term for the current goal is Hmono.
We prove the intermediate claim Hcofinal0: ∀j : set, j ∈ (net_pack_index N) → ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ (net_pack_le N).
We prove the intermediate claim Hcofinal: ∀j : set, j ∈ (net_pack_index Ni) → ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ (net_pack_le Ni).
An exact proof term for the current goal is (subnet_of_witness_cofinal (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
rewrite the current goal using HNiidx (from right to left).
rewrite the current goal using HNile (from right to left).
An exact proof term for the current goal is Hcofinal.
We prove the intermediate claim Hwsub: subnet_of_witness (net_pack_fun N) netSw (net_pack_index N) (net_pack_le N) K leK (product_space I Xi) phi.
An exact proof term for the current goal is (subnet_of_witness_compose_fun (net_pack_fun N) (net_pack_index N) (net_pack_le N) K leK (product_space I Xi) phi HdirN0 HdirK HtotN0 HgraphN0 HdomN0 Htotphi0 Hgraphphi0 Hdomphi0 Hmono0 Hcofinal0).
We prove the intermediate claim HSwdef: Sw = net_pack K leK netSw.
Use reflexivity.
We prove the intermediate claim HSwfun: net_pack_fun Sw = netSw.
rewrite the current goal using HSwdef (from left to right).
An exact proof term for the current goal is (net_pack_fun_eq K leK netSw).
We prove the intermediate claim HSwidx: net_pack_index Sw = K.
rewrite the current goal using HSwdef (from left to right).
An exact proof term for the current goal is (net_pack_index_eq K leK netSw).
We prove the intermediate claim HSwle: net_pack_le Sw = leK.
rewrite the current goal using HSwdef (from left to right).
An exact proof term for the current goal is (net_pack_le_eq K leK netSw).
We prove the intermediate claim Hwsub0: subnet_of_witness (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi.
rewrite the current goal using HSwfun (from left to right).
rewrite the current goal using HSwidx (from left to right).
rewrite the current goal using HSwle (from left to right).
An exact proof term for the current goal is Hwsub.
An exact proof term for the current goal is Hwsub0.
Set Xi0 to be the term space_family_set Xi (pickI w).
Set Ti0 to be the term space_family_topology Xi (pickI w).
We prove the intermediate claim HconvSi: net_pack_converges Xi0 Ti0 Si (apply_fun x (pickI w)).
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w)))) 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 HconvOnSi: net_converges_on Xi0 Ti0 (net_pack_fun Si) (net_pack_index Si) (net_pack_le Si) (apply_fun x (pickI w)).
Apply HconvSi to the current goal.
Let J0 be given.
Assume Hexle0: ∃le0 net0 : set, Si = net_pack J0 le0 net0 ∧ net_converges_on Xi0 Ti0 net0 J0 le0 (apply_fun x (pickI w)).
Apply Hexle0 to the current goal.
Let le0 be given.
Assume Hexnet0: ∃net0 : set, Si = net_pack J0 le0 net0 ∧ net_converges_on Xi0 Ti0 net0 J0 le0 (apply_fun x (pickI w)).
Apply Hexnet0 to the current goal.
Let net0 be given.
Assume Hpair: Si = net_pack J0 le0 net0 ∧ net_converges_on Xi0 Ti0 net0 J0 le0 (apply_fun x (pickI w)).
We prove the intermediate claim HSiDef: Si = net_pack J0 le0 net0.
An exact proof term for the current goal is (andEL (Si = net_pack J0 le0 net0) (net_converges_on Xi0 Ti0 net0 J0 le0 (apply_fun x (pickI w))) Hpair).
We prove the intermediate claim HSiConv: net_converges_on Xi0 Ti0 net0 J0 le0 (apply_fun x (pickI w)).
An exact proof term for the current goal is (andER (Si = net_pack J0 le0 net0) (net_converges_on Xi0 Ti0 net0 J0 le0 (apply_fun x (pickI w))) Hpair).
rewrite the current goal using HSiDef (from left to right).
rewrite the current goal using (net_pack_fun_eq J0 le0 net0) (from left to right).
rewrite the current goal using (net_pack_index_eq J0 le0 net0) (from left to right).
rewrite the current goal using (net_pack_le_eq J0 le0 net0) (from left to right).
An exact proof term for the current goal is HSiConv.
We prove the intermediate claim HdirK0: directed_set K leK.
An exact proof term for the current goal is (subnet_of_witness_dirK (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
We prove the intermediate claim HSwdef0: Sw = net_pack K leK netSw.
Use reflexivity.
We prove the intermediate claim HSwidx0: net_pack_index Sw = K.
rewrite the current goal using HSwdef0 (from left to right).
An exact proof term for the current goal is (net_pack_index_eq K leK netSw).
We prove the intermediate claim HSwle0: net_pack_le Sw = leK.
rewrite the current goal using HSwdef0 (from left to right).
An exact proof term for the current goal is (net_pack_le_eq K leK netSw).
We prove the intermediate claim HSwfun0: net_pack_fun Sw = netSw.
rewrite the current goal using HSwdef0 (from left to right).
An exact proof term for the current goal is (net_pack_fun_eq K leK netSw).
Set coordNet to be the term compose_fun K netSw (product_eval_map I Xi (pickI w)).
We prove the intermediate claim HcoordNetDef: compose_fun (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w)) = coordNet.
rewrite the current goal using HSwidx0 (from left to right).
rewrite the current goal using HSwfun0 (from left to right).
Use reflexivity.
rewrite the current goal using HcoordNetDef (from left to right).
rewrite the current goal using HSwidx0 (from left to right).
rewrite the current goal using HSwle0 (from left to right).
We prove the intermediate claim HTi0: topology_on Xi0 Ti0.
Apply (and7E (topology_on Xi0 Ti0) (directed_set (net_pack_index Si) (net_pack_le Si)) (total_function_on (net_pack_fun Si) (net_pack_index Si) Xi0) (functional_graph (net_pack_fun Si)) (graph_domain_subset (net_pack_fun Si) (net_pack_index Si)) (apply_fun x (pickI w) ∈ Xi0) (∀U : set, U ∈ Ti0 → apply_fun x (pickI w) ∈ U → ∃i0 : set, i0 ∈ (net_pack_index Si) ∧ ∀i : set, i ∈ (net_pack_index Si) → (i0,i) ∈ (net_pack_le Si) → apply_fun (net_pack_fun Si) i ∈ U) HconvOnSi (topology_on Xi0 Ti0)) to the current goal.
Assume H1 H2 H3 H4 H5 H6 H7.
An exact proof term for the current goal is H1.
We prove the intermediate claim HtotSi: total_function_on (net_pack_fun Si) K Xi0.
Apply (and7E (topology_on Xi0 Ti0) (directed_set K leK) (total_function_on (net_pack_fun Si) K Xi0) (functional_graph (net_pack_fun Si)) (graph_domain_subset (net_pack_fun Si) K) (apply_fun x (pickI w) ∈ Xi0) (∀U : set, U ∈ Ti0 → apply_fun x (pickI w) ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun (net_pack_fun Si) i ∈ U) HconvOnSi (total_function_on (net_pack_fun Si) K Xi0)) to the current goal.
Assume H1 H2 H3 H4 H5 H6 H7.
An exact proof term for the current goal is H3.
We prove the intermediate claim HtailSi: ∀U : set, U ∈ Ti0 → apply_fun x (pickI w) ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun (net_pack_fun Si) i ∈ U.
Apply (and7E (topology_on Xi0 Ti0) (directed_set K leK) (total_function_on (net_pack_fun Si) K Xi0) (functional_graph (net_pack_fun Si)) (graph_domain_subset (net_pack_fun Si) K) (apply_fun x (pickI w) ∈ Xi0) (∀U : set, U ∈ Ti0 → apply_fun x (pickI w) ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun (net_pack_fun Si) i ∈ U) HconvOnSi (∀U : set, U ∈ Ti0 → apply_fun x (pickI w) ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun (net_pack_fun Si) i ∈ U)) to the current goal.
Assume H1 H2 H3 H4 H5 H6 H7.
An exact proof term for the current goal is H7.
We prove the intermediate claim HvalsSi: ∀k : set, k ∈ K → apply_fun (net_pack_fun Si) k = apply_fun (net_pack_fun Ni) (apply_fun phi k).
An exact proof term for the current goal is (subnet_of_witness_vals (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
We prove the intermediate claim HNiidx0: net_pack_index Ni = net_pack_index N.
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (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.
We prove the intermediate claim HNile0: net_pack_le Ni = net_pack_le N.
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (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.
We prove the intermediate claim HNiCanon0: 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) (pickI w))).
Apply (and6E (net_pack_in_space (space_family_set Xi (pickI w)) 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) (pickI w)))) (subnet_pack_of_in (space_family_set Xi (pickI w)) Ni Si) (net_pack_converges (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) Si (apply_fun x (pickI w))) Hpack (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) (pickI w))))) to the current goal.
Assume H1 H2 H3 H4 H5 H6.
An exact proof term for the current goal is H4.
We prove the intermediate claim HtotphiN: total_function_on phi K (net_pack_index N).
We prove the intermediate claim HtotphiNi: total_function_on phi K (net_pack_index Ni).
An exact proof term for the current goal is (subnet_of_witness_totphi (net_pack_fun Ni) (net_pack_fun Si) (net_pack_index Ni) (net_pack_le Ni) K leK (space_family_set Xi (pickI w)) phi Hwphi).
rewrite the current goal using HNiidx0 (from right to left).
An exact proof term for the current goal is HtotphiNi.
We prove the intermediate claim HNiFunCanon: net_pack_fun Ni = graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) (pickI w)).
rewrite the current goal using HNiCanon0 (from left to right).
An exact proof term for the current goal is (net_pack_fun_eq (net_pack_index N) (net_pack_le N) (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) (pickI w)))).
We prove the intermediate claim HtotN0: total_function_on (net_pack_fun N) (net_pack_index N) (product_space I Xi).
rewrite the current goal using HNfun (from left to right).
rewrite the current goal using HNidx (from left to right).
An exact proof term for the current goal is HNtot.
We prove the intermediate claim HcoordVal: ∀k : set, k ∈ K → apply_fun coordNet k = apply_fun (net_pack_fun Si) k.
Let k be given.
Assume HkK: k ∈ K.
We prove the intermediate claim Hcdef: coordNet = graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0)).
Use reflexivity.
rewrite the current goal using Hcdef (from left to right).
We prove the intermediate claim HappCoord: apply_fun (graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0))) k = apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k).
An exact proof term for the current goal is (apply_fun_graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0)) k HkK).
rewrite the current goal using HappCoord (from left to right).
We prove the intermediate claim Hnsdef: netSw = graph K (λk0 : set ⇒ apply_fun (net_pack_fun N) (apply_fun phi k0)).
Use reflexivity.
We prove the intermediate claim HnetSwk: apply_fun netSw k = apply_fun (net_pack_fun N) (apply_fun phi k).
rewrite the current goal using Hnsdef (from left to right).
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ apply_fun (net_pack_fun N) (apply_fun phi k0)) k HkK) (from left to right).
Use reflexivity.
rewrite the current goal using HnetSwk (from left to right).
We prove the intermediate claim HphikJ: apply_fun phi k ∈ net_pack_index N.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K (net_pack_index N) k HtotphiN HkK).
We prove the intermediate claim HNkX: apply_fun (net_pack_fun N) (apply_fun phi k) ∈ product_space I Xi.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y (net_pack_fun N) (net_pack_index N) (product_space I Xi) (apply_fun phi k) HtotN0 HphikJ).
We prove the intermediate claim HappEval: apply_fun (product_eval_map I Xi (pickI w)) (apply_fun (net_pack_fun N) (apply_fun phi k)) = apply_fun (apply_fun (net_pack_fun N) (apply_fun phi k)) (pickI w).
We prove the intermediate claim HevalDef: product_eval_map I Xi (pickI w) = graph (product_space I Xi) (λf0 : set ⇒ apply_fun f0 (pickI w)).
Use reflexivity.
rewrite the current goal using HevalDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (product_space I Xi) (λf0 : set ⇒ apply_fun f0 (pickI w)) (apply_fun (net_pack_fun N) (apply_fun phi k)) HNkX).
rewrite the current goal using HappEval (from left to right).
rewrite the current goal using (HvalsSi k HkK) (from left to right).
rewrite the current goal using HNiFunCanon (from left to right).
We prove the intermediate claim HphikN: apply_fun phi k ∈ net_pack_index N.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K (net_pack_index N) k HtotphiN HkK).
We prove the intermediate claim HappNi: apply_fun (graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) (pickI w))) (apply_fun phi k) = apply_fun (apply_fun (net_pack_fun N) (apply_fun phi k)) (pickI w).
An exact proof term for the current goal is (apply_fun_graph (net_pack_index N) (λj : set ⇒ apply_fun (apply_fun (net_pack_fun N) j) (pickI w)) (apply_fun phi k) HphikN).
rewrite the current goal using HappNi (from left to right).
Use reflexivity.
Apply (and7I (topology_on Xi0 Ti0) (directed_set K leK) (total_function_on coordNet K Xi0) (functional_graph coordNet) (graph_domain_subset coordNet K) (apply_fun x (pickI w) ∈ Xi0) (∀U : set, U ∈ Ti0 → apply_fun x (pickI w) ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun coordNet i ∈ U)) to the current goal.
An exact proof term for the current goal is HTi0.
An exact proof term for the current goal is HdirK0.
Apply (total_function_on_graph K Xi0 (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0))) to the current goal.
Let k be given.
Assume HkK: k ∈ K.
We prove the intermediate claim Hcdef0: coordNet = graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0)).
Use reflexivity.
We prove the intermediate claim HcoordAp0: apply_fun coordNet k = apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k).
rewrite the current goal using Hcdef0 (from left to right).
An exact proof term for the current goal is (apply_fun_graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0)) k HkK).
We prove the intermediate claim HcoordAp0': apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k) = apply_fun coordNet k.
rewrite the current goal using Hcdef0 (from left to right).
We prove the intermediate claim HappCoord0: apply_fun (graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0))) k = apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k).
An exact proof term for the current goal is (apply_fun_graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0)) k HkK).
rewrite the current goal using HappCoord0 (from left to right).
Use reflexivity.
We prove the intermediate claim Hbeta0: (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0)) k = apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k).
Use reflexivity.
rewrite the current goal using Hbeta0 (from left to right).
rewrite the current goal using HcoordAp0' (from left to right).
We prove the intermediate claim HvalSi: apply_fun (net_pack_fun Si) k ∈ Xi0.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y (net_pack_fun Si) K Xi0 k HtotSi HkK).
We prove the intermediate claim HeqCoord: apply_fun coordNet k = apply_fun (net_pack_fun Si) k.
An exact proof term for the current goal is (HcoordVal k HkK).
rewrite the current goal using HeqCoord (from left to right).
An exact proof term for the current goal is HvalSi.
An exact proof term for the current goal is (functional_graph_graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0))).
An exact proof term for the current goal is (graph_domain_subset_graph K (λk0 : set ⇒ apply_fun (product_eval_map I Xi (pickI w)) (apply_fun netSw k0))).
We prove the intermediate claim HiwI: pickI w ∈ I.
An exact proof term for the current goal is (andEL (pickI w ∈ I) (idx (pickI w) = w) (HpickI w HwW)).
An exact proof term for the current goal is (Hxcoord (pickI w) HiwI).
Let U be given.
Assume HU: U ∈ Ti0.
Assume HxU: apply_fun x (pickI w) ∈ U.
Apply (HtailSi U HU HxU) to the current goal.
Let i0 be given.
Assume Hi0pair.
Apply Hi0pair to the current goal.
Assume Hi0K Hafter.
We use i0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0K.
Let i be given.
Assume HiK: i ∈ K.
Assume Hi0i: (i0,i) ∈ leK.
We prove the intermediate claim HSiU: apply_fun (net_pack_fun Si) i ∈ U.
An exact proof term for the current goal is (Hafter i HiK Hi0i).
We prove the intermediate claim HeqCoordi: apply_fun coordNet i = apply_fun (net_pack_fun Si) i.
An exact proof term for the current goal is (HcoordVal i HiK).
rewrite the current goal using HeqCoordi (from left to right).
An exact proof term for the current goal is HSiU.
We prove the intermediate claim Hcoord_nbhd_cofinal: ∀w U j0 : set, w ∈ W → U ∈ space_family_topology Xi (pickI w) → apply_fun x (pickI w) ∈ U → j0 ∈ net_pack_index N → ∃j : set, j ∈ net_pack_index N ∧ (j0,j) ∈ net_pack_le N ∧ apply_fun (apply_fun (net_pack_fun N) j) (pickI w) ∈ U.
Let w be given.
Let U be given.
Let j0 be given.
Assume HwW: w ∈ W.
Assume HU: U ∈ space_family_topology Xi (pickI w).
Assume HxU: apply_fun x (pickI w) ∈ U.
Assume Hj0J: j0 ∈ net_pack_index N.
Apply (HliftWsub w HwW) to the current goal.
Let Sw be given.
Assume HSwpair.
We prove the intermediate claim HSwsub: subnet_pack_of_in (product_space I Xi) N Sw.
An exact proof term for the current goal is (andEL (subnet_pack_of_in (product_space I Xi) N Sw) (net_converges_on (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) (compose_fun (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w))) (net_pack_index Sw) (net_pack_le Sw) (apply_fun x (pickI w))) HSwpair).
We prove the intermediate claim HSwconv: net_converges_on (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) (compose_fun (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w))) (net_pack_index Sw) (net_pack_le Sw) (apply_fun x (pickI w)).
An exact proof term for the current goal is (andER (subnet_pack_of_in (product_space I Xi) N Sw) (net_converges_on (space_family_set Xi (pickI w)) (space_family_topology Xi (pickI w)) (compose_fun (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w))) (net_pack_index Sw) (net_pack_le Sw) (apply_fun x (pickI w))) HSwpair).
Set Xi0 to be the term space_family_set Xi (pickI w).
Set Ti0 to be the term space_family_topology Xi (pickI w).
Set coordNet to be the term compose_fun (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w)).
Apply HSwconv to the current goal.
Assume HconvCore HconvTail.
Apply HconvCore to the current goal.
Assume HconvCore5 HxXi0.
Apply HconvCore5 to the current goal.
Assume HconvCore4 HdomSw.
Apply HconvCore4 to the current goal.
Assume HconvCore3 HgraphSw.
Apply HconvCore3 to the current goal.
Assume HconvCore2 HtotSw.
Apply HconvCore2 to the current goal.
Assume HTi0 HdirK.
Apply (HconvTail U HU HxU) to the current goal.
Let kU be given.
Assume HkUpair.
Apply HkUpair to the current goal.
Assume HkUK HafterU.
Apply HSwsub to the current goal.
Let phi be given.
Assume Hwsub: subnet_of_witness (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi.
We prove the intermediate claim Htotphi: total_function_on phi (net_pack_index Sw) (net_pack_index N).
An exact proof term for the current goal is (subnet_of_witness_totphi (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi Hwsub).
We prove the intermediate claim HvalsSw: ∀k : set, k ∈ net_pack_index Sw → apply_fun (net_pack_fun Sw) k = apply_fun (net_pack_fun N) (apply_fun phi k).
An exact proof term for the current goal is (subnet_of_witness_vals (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi Hwsub).
We prove the intermediate claim HtailAbove: ∃k0 : set, k0 ∈ net_pack_index Sw ∧ ∀k : set, k ∈ net_pack_index Sw → (k0,k) ∈ net_pack_le Sw → (j0,apply_fun phi k) ∈ net_pack_le N.
An exact proof term for the current goal is (subnet_of_witness_tail_above (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi j0 Hwsub Hj0J).
Apply HtailAbove to the current goal.
Let k0 be given.
Assume Hk0pair.
We prove the intermediate claim Hk0K: k0 ∈ net_pack_index Sw.
An exact proof term for the current goal is (andEL (k0 ∈ net_pack_index Sw) (∀k : set, k ∈ net_pack_index Sw → (k0,k) ∈ net_pack_le Sw → (j0,apply_fun phi k) ∈ net_pack_le N) Hk0pair).
We prove the intermediate claim Hk0prop: ∀k : set, k ∈ net_pack_index Sw → (k0,k) ∈ net_pack_le Sw → (j0,apply_fun phi k) ∈ net_pack_le N.
An exact proof term for the current goal is (andER (k0 ∈ net_pack_index Sw) (∀k : set, k ∈ net_pack_index Sw → (k0,k) ∈ net_pack_le Sw → (j0,apply_fun phi k) ∈ net_pack_le N) Hk0pair).
Apply (directed_set_upper_bound_property (net_pack_index Sw) (net_pack_le Sw) HdirK kU k0 HkUK Hk0K) to the current goal.
Let k1 be given.
Assume Hk1pack.
We prove the intermediate claim Hk1K: k1 ∈ net_pack_index Sw.
Apply (and3E (k1 ∈ net_pack_index Sw) ((kU,k1) ∈ net_pack_le Sw) ((k0,k1) ∈ net_pack_le Sw) Hk1pack (k1 ∈ net_pack_index Sw)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H1.
We prove the intermediate claim HkUk1: (kU,k1) ∈ net_pack_le Sw.
Apply (and3E (k1 ∈ net_pack_index Sw) ((kU,k1) ∈ net_pack_le Sw) ((k0,k1) ∈ net_pack_le Sw) Hk1pack ((kU,k1) ∈ net_pack_le Sw)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H2.
We prove the intermediate claim Hk0k1: (k0,k1) ∈ net_pack_le Sw.
Apply (and3E (k1 ∈ net_pack_index Sw) ((kU,k1) ∈ net_pack_le Sw) ((k0,k1) ∈ net_pack_le Sw) Hk1pack ((k0,k1) ∈ net_pack_le Sw)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H3.
Set j to be the term apply_fun phi k1.
We use j to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HjJ: j ∈ net_pack_index N.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi (net_pack_index Sw) (net_pack_index N) k1 Htotphi Hk1K).
An exact proof term for the current goal is HjJ.
We prove the intermediate claim Hjdef: j = apply_fun phi k1.
Use reflexivity.
rewrite the current goal using Hjdef (from left to right).
An exact proof term for the current goal is (Hk0prop k1 Hk1K Hk0k1).
We prove the intermediate claim HcoordU: apply_fun coordNet k1 ∈ U.
An exact proof term for the current goal is (HafterU k1 Hk1K HkUk1).
We prove the intermediate claim HtotSwNet: total_function_on (net_pack_fun Sw) (net_pack_index Sw) (product_space I Xi).
An exact proof term for the current goal is (subnet_of_witness_totsub (net_pack_fun N) (net_pack_fun Sw) (net_pack_index N) (net_pack_le N) (net_pack_index Sw) (net_pack_le Sw) (product_space I Xi) phi Hwsub).
We prove the intermediate claim HSwk1X: apply_fun (net_pack_fun Sw) k1 ∈ product_space I Xi.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y (net_pack_fun Sw) (net_pack_index Sw) (product_space I Xi) k1 HtotSwNet Hk1K).
We prove the intermediate claim HcompAp: apply_fun coordNet k1 = apply_fun (product_eval_map I Xi (pickI w)) (apply_fun (net_pack_fun Sw) k1).
An exact proof term for the current goal is (compose_fun_apply (net_pack_index Sw) (net_pack_fun Sw) (product_eval_map I Xi (pickI w)) k1 Hk1K).
We prove the intermediate claim HappEval: apply_fun (product_eval_map I Xi (pickI w)) (apply_fun (net_pack_fun Sw) k1) = apply_fun (apply_fun (net_pack_fun Sw) k1) (pickI w).
An exact proof term for the current goal is (apply_fun_graph (product_space I Xi) (λg : set ⇒ apply_fun g (pickI w)) (apply_fun (net_pack_fun Sw) k1) HSwk1X).
We prove the intermediate claim HSwcoordU: apply_fun (apply_fun (net_pack_fun Sw) k1) (pickI w) ∈ U.
rewrite the current goal using HappEval (from right to left).
rewrite the current goal using HcompAp (from right to left).
An exact proof term for the current goal is HcoordU.
We prove the intermediate claim HNphi: apply_fun (net_pack_fun Sw) k1 = apply_fun (net_pack_fun N) j.
An exact proof term for the current goal is (HvalsSw k1 Hk1K).
rewrite the current goal using HNphi (from right to left) at position 1.
An exact proof term for the current goal is HSwcoordU.
The rest of this subproof is missing.
∎