proposition: Lemma inl_prod__uu_comp (E := inductive_limit SE) (E' := inductive_limit SE') (F := inductive_limit SF) (F' := inductive_limit SF') (EE:= inductive_limit (inl_system_product si1)) (FF:= inductive_limit (inl_system_product si3)) (lu:= inductive_limit_fun SE SF u) (lu':= inductive_limit_fun SE' SF' u') (luu:= inductive_limit_fun inl_prod_SEE inl_prod_SFF inl_prod_uu) (idEE := inductive_map (inl_system_product si1) (inl_product_can_fun SE SE') (E \times E')) (idFF := inductive_map (inl_system_product si3) (inl_product_can_fun SF SF') (F \times F')): [/\ bijection_prop idEE EE (E \times E'), bijection_prop idFF FF (F \times F'), function_prop (lu \ftimes lu') (E \times E') (F \times F'), function_prop luu EE FF & (lu \ftimes lu') \co idEE = idFF \co luu].
proof: Proof. move:(inl_product_can_fun_bij si1); rewrite /= -/E -/E' -/EE -/idEE => pa. move:(inl_product_can_fun_bij si3); rewrite /= -/F -/F' -/FF -/idFF => pb. move:(proj1 (inl_map2_prop si2 cu)); rewrite -/E -/F -/lu => lup. move:(proj1 (inl_map2_prop inl_prod_si4 cu')). rewrite -/E' -/F' -/lu'; move => lup'. move: (ext_to_prod_fun_bis lup lup') => pc. have si5: inl_same_index inl_prod_SEE inl_prod_SFF by []. move: (proj1 (inl_map2_prop si5 inl_prod_uu_prop)). rewrite -/EE -/FF -/luu => pd. split => //. move:pa pb => [[[fiE _] _] siE tiE] [[[fiF _] _] siF tiF]. move:pc pd => [fh sh th] [fb sb tb]. have cop1: lu \ftimes lu' \coP idEE by split => //; ue. have cop2: idFF \coP luu by split => //; ue. apply: function_exten. - by apply:compf_f. - by apply:compf_f. - aw; ue. - aw; ue. - aw; rewrite siE => x xE. have xs1:inc x (source luu) by ue. have xs2: inc x (source idEE) by ue. move:lup lup' => [fu su tu][fu' su' tu']. rewrite ! compfV //. move/inductive_limit_hi: xE; move => /= []. set i := (Q (rep x)); set y := (P (rep x));move => iIE qb ->. have iIE': inc i (isI SE') by rewrite - (inl_same_index_same_I si1). have iIF: inc i (isI SF) by rewrite - (inl_same_index_same_I si2). have iIF': inc i (isI SF') by rewrite - (inl_same_index_same_I si3). have ra:= (inl_product_can_fun_compat si1). have ra':= (inl_product_can_fun_compat si3). rewrite (inl_inductive_map_ev ra iIE qb). rewrite /inl_product_can_fun LgV//. move:(inl_can_fun_fp iIE) => [fcfi scfi tcfi]. move:(inl_can_fun_fp iIE') => [fcfi' scfi' tcfi']. rewrite (inl_map_val_aux2 si5 inl_prod_uu_prop iIE qb). rewrite /inl_prod_uu LgV//. move:(proj43 cu i iIE) => [fui sui tui]. move:(proj43 cu' i iIE') => [fui' sui' tui']. move:qb; rewrite /inl_product_E LgV// => qb. have ys:inc y (source (Vg u i) \times source (Vg u' i)) by rewrite sui sui'. rewrite (ext_to_prod_V2 fui fui' ys). move: (qb); rewrite - scfi - scfi' => qb'. move /setX_P: qb => [py Py Qy]. have rx:inc (J (Vf (Vg u i) (P y)) (Vf (Vg u' i) (Q y))) (Vg (isE (inl_system_product si3)) i). rewrite /= /inl_product_E LgV//; apply:setXp_i; Wtac. rewrite (inl_inductive_map_ev ra' iIF rx). rewrite /inl_product_can_fun !LgV//. move: (inl_can_fun_fp iIF) => [fcfi''' scfi''' tcfi''']. move: (inl_can_fun_fp iIF') => [fcfi'''' scfi'''' tcfi'''']. have rb: inc (Vf (Vg u i) (P y)) (Vg (isE SF) i) by Wtac. have rc: inc (Vf (Vg u' i) (Q y)) (Vg (isE SF') i) by Wtac. rewrite (ext_to_prod_V fcfi''' fcfi''''); try ue. rewrite (inl_can_fun_ev iIF rb) (inl_can_fun_ev iIF' rc). rewrite (ext_to_prod_V2 fcfi fcfi' qb'). rewrite (inl_can_fun_ev iIE Py) (inl_can_fun_ev iIE' Qy). have rb':= (inl_class_in_lim iIE Py). have rc':=(inl_class_in_lim iIE' Qy). have si4:= inl_prod_si4. rewrite (ext_to_prod_V fu fu'); try ue. rewrite (inl_map_val_aux2 si2 cu iIE Py) (inl_map_val_aux2 si4 cu' iIE' Qy). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)