Let I, Xi, N and i be given.
Assume HN: net_pack_in_space (product_space I Xi) N.
Assume HiI: i ∈ I.
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 (product_space I Xi) ∧ 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 (product_space I Xi) ∧ functional_graph net ∧ graph_domain_subset net J.
Apply Hexnet to the current goal.
Let net be given.
Assume Hdata: N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J (product_space I Xi) ∧ functional_graph net ∧ graph_domain_subset net J.
Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J (product_space I Xi)) (functional_graph net) (graph_domain_subset net J) Hdata) to the current goal.
Assume HNdef Hdir Htot Hgraph Hdom.
Set projnet to be the term graph J (λj : set ⇒ apply_fun (apply_fun net j) i).
Set Ni to be the term net_pack J le projnet.
We use Ni to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove net_pack_in_space (space_family_set Xi i) Ni.
We will prove ∃J0 le0 net0 : set, Ni = net_pack J0 le0 net0 ∧ directed_set J0 le0 ∧ total_function_on net0 J0 (space_family_set Xi i) ∧ 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 projnet to witness the existential quantifier.
Apply (and5I (Ni = net_pack J le projnet) (directed_set J le) (total_function_on projnet J (space_family_set Xi i)) (functional_graph projnet) (graph_domain_subset projnet J)) to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hdir.
We prove the intermediate claim Hg: ∀j : set, j ∈ J → apply_fun (apply_fun net j) i ∈ space_family_set Xi i.
Let j be given.
Assume HjJ: j ∈ J.
We prove the intermediate claim HnetjXp: apply_fun net j ∈ product_space I Xi.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y net J (product_space I Xi) j Htot HjJ).
We prove the intermediate claim Hprop: total_function_on (apply_fun net j) I (space_family_union I Xi) ∧ functional_graph (apply_fun net j) ∧ ∀k : set, k ∈ I → apply_fun (apply_fun net j) k ∈ space_family_set Xi k.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf : set ⇒ total_function_on f I (space_family_union I Xi) ∧ functional_graph f ∧ ∀k : set, k ∈ I → apply_fun f k ∈ space_family_set Xi k) (apply_fun net j) HnetjXp).
We prove the intermediate claim Hcoords: ∀k : set, k ∈ I → apply_fun (apply_fun net j) k ∈ space_family_set Xi k.
An exact proof term for the current goal is (andER (total_function_on (apply_fun net j) I (space_family_union I Xi) ∧ functional_graph (apply_fun net j)) (∀k : set, k ∈ I → apply_fun (apply_fun net j) k ∈ space_family_set Xi k) Hprop).
An exact proof term for the current goal is (Hcoords i HiI).
We prove the intermediate claim Hprojdef: projnet = graph J (λj : set ⇒ apply_fun (apply_fun net j) i).
Use reflexivity.
rewrite the current goal using Hprojdef (from left to right).
An exact proof term for the current goal is (total_function_on_graph J (space_family_set Xi i) (λj : set ⇒ apply_fun (apply_fun net j) i) Hg).
An exact proof term for the current goal is (functional_graph_graph J (λj : set ⇒ apply_fun (apply_fun net j) i)).
An exact proof term for the current goal is (graph_domain_subset_graph J (λj : set ⇒ apply_fun (apply_fun net j) i)).
We prove the intermediate claim HidxNi: net_pack_index Ni = J.
rewrite the current goal using (net_pack_index_eq J le projnet) (from left to right).
Use reflexivity.
We prove the intermediate claim HidxN: net_pack_index N = J.
rewrite the current goal using HNdef (from left to right).
An exact proof term for the current goal is (net_pack_index_eq J le net).
rewrite the current goal using HidxNi (from left to right).
rewrite the current goal using HidxN (from right to left).
Use reflexivity.
We prove the intermediate claim HleNi: net_pack_le Ni = le.
rewrite the current goal using (net_pack_le_eq J le projnet) (from left to right).
Use reflexivity.
We prove the intermediate claim HleN: net_pack_le N = le.
rewrite the current goal using HNdef (from left to right).
An exact proof term for the current goal is (net_pack_le_eq J le net).
rewrite the current goal using HleNi (from left to right).
rewrite the current goal using HleN (from right to left).
Use reflexivity.
We prove the intermediate claim Hprojdef: projnet = graph J (λj0 : set ⇒ apply_fun (apply_fun net j0) i).
Use reflexivity.
rewrite the current goal using Hprojdef (from left to right).
rewrite the current goal using HNdef (from left to right).
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.
∎