proposition: Lemma inl_product_can_fun_bij S S' (sd: inl_same_index S S') (E:= inductive_limit S) (E' := inductive_limit S') (f:= inductive_map (inl_system_product sd) (inl_product_can_fun S S') (E \times E')): bijection_prop f (inductive_limit (inl_system_product sd)) (E \times E').
proof: Proof. move:(inl_system_product_prop sd) => [pa pb pc pd]. move:(inl_product_can_fun_compat sd) => ha. move:(inl_map_prop ha) (inl_map_ax ha). have ssI:= (inl_same_index_same_I sd). rewrite -/E -/E' -/f; move =>[hc hd ] he. rewrite /f/inductive_map; saw. split. apply/(inl_map_injective ha); move => i x y /= iI. rewrite/inl_product_E/inl_product_can_fun. rewrite !LgV//. move => /setX_P [px Px Qx] /setX_P [py Py Qy]. move: (inl_can_fun_fp iI) => [fi si ti]. move:(iI); rewrite ssI => iI'. move: (inl_can_fun_fp iI') => [fi' si' ti']. have ra: inc (P y) (source (inl_can_fun S i)) by ue. have rb: inc (Q y) (source (inl_can_fun S' i)) by ue. have rc: inc (P x) (source (inl_can_fun S i)) by ue. have rd: inc (Q x) (source (inl_can_fun S' i)) by ue. rewrite -px - py ext_to_prod_V // ext_to_prod_V //. do 4 rewrite inl_can_fun_ev //. move => eq1; move:(pr1_def eq1) (pr2_def eq1); clear eq1. move/(inl_class_eq_bis iI iI Px Py) => [k []]; aw => lik _ eq2. move/(inl_class_eq_bis iI' iI' Qx Qy) => [k' []]; aw => lik' _ eq2'. move:(proj2(inl_prop0 lik)) (proj2(inl_prop0 lik')); rewrite - ssI => kI kI'. move: (is_directed_r kI kI') => [l [lI lkl lkl']]. move: (proj33 (is_preorder_r S) _ _ _ lik lkl) => lil. move:(inl_prop4 lil) => [fil sil til]. move:(lil); rewrite sd => lil'; rewrite sd in lkl'. move:(inl_prop4 lil') => [fil' sil' til']. have ra': inc (P y) (source (Vg (isf S) (J i l))) by ue. have rb': inc (Q y) (source (Vg (isf S') (J i l))) by ue. have rc': inc (P x) (source (Vg (isf S) (J i l))) by ue. have rd': inc (Q x) (source (Vg (isf S') (J i l))) by ue. exists l => //=. rewrite /inl_product_f LgV// ext_to_prod_V // ext_to_prod_V //. rewrite -(inl_prop3 lik lkl Px) - (inl_prop3 lik lkl Py) eq2. by rewrite -(inl_prop3 lik' lkl' Qx) - (inl_prop3 lik' lkl' Qy) eq2'. apply:lf_surjective => // y /setX_P[py Py Qy]. move/inductive_limit_hi:Py => [sa sb sc]. move/inductive_limit_hi:Qy => [sa' sb' sc']. rewrite - ssI in sa'. move:(is_directed_r sa sa') => [k [kI lik ljk]]. move: sc; rewrite -(inl_class_of_fij lik sb); set y1 := Vf _ _ => Py. rewrite sd in ljk. move: sc'; rewrite-(inl_class_of_fij ljk sb'); set y2 := Vf _ _ => Qy. move:(inl_can_fun_fp kI) => [fk sk tk]. move:(kI); rewrite ssI => kI'. move:(inl_can_fun_fp kI') => [fk' sk' tk']. have ra: inc y2 (Vg (isE S') k). move:(inl_prop4 ljk) => [ff sf tf];rewrite /y2; Wtac. have rb: inc y2 (source (inl_can_fun S' k)) by ue. have rc : inc y1 (Vg (isE S) k). move:(inl_prop4 lik) => [ff sf tf];rewrite /y1; Wtac. have rd: inc y1 (source (inl_can_fun S k)) by ue. have pE:inc (J y1 y2) (Vg (isE (inl_system_product sd)) k). by rewrite /= /inl_product_E LgV//; apply: setXp_i. set x := (class (inl_equiv (inl_system_product sd)) (J (J y1 y2) k)). have xl: inc x (inductive_limit (inl_system_product sd)). by apply: (inl_class_in_lim). exists x => //. move:(inl_map_property_res1 ha (inl_map_prop ha) kI pE). rewrite /inductive_map LfV// => ->; rewrite /inl_product_can_fun LgV//. by rewrite ext_to_prod_V // inl_can_fun_ev // inl_can_fun_ev // - Py - Qy py. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)