proposition: Lemma inl_Lemma5_1i S X (K:= domain X) (Y := fun a => Lg K (fun i => Vf (Vg (isf S) (J (Q (rep (Vg X i))) a)) (P (rep (Vg X i))))): fgraph X -> finite_set K -> nonempty K -> (forall i, inc i K -> inc (Vg X i) (inductive_limit S)) -> exists2 a, inc a (isI S) & [/\ fgraph (Y a), domain (Y a) = K & forall i, inc i K -> Vg X i = Vf (inl_can_fun S a) (Vg (Y a) i) ].
proof: Proof. move => fgX fsK neK XE. have ha: forall i, inc i K -> inc (Q (rep (Vg X i))) (isI S). by move => i /XE /inductive_limitP []; rewrite inl_equiv_sr; case/inl_sumP. set IK := fun_image K (fun i => (Q (rep (Vg X i)))). have neik: nonempty IK by apply:funI_setne. have fsk: finite_set IK by apply: finite_fun_image. have sik: sub IK (isI S) by move => t/ funI_P [z zK ->]; apply: ha. move: (finite_preorder_directed_bounded (is_preorder_r S) (is_substrate_r S) (@is_directed_r S) neik fsk sik) => [a aI ap]. ex_tac. have ap2 i: inc i K -> gle (isr S) (Q (rep (Vg X i))) a. move => iK; apply:ap; apply/funI_P; ex_tac. rewrite /Y;split; aww => i iK; rewrite LgV//. move: (XE _ iK) => /inductive_limit_hi [pa pb {1} ->]. set y := (Vf (Vg _ _) _). have yiE: inc y (Vg (isE S) a). move:(inl_prop4 (ap2 _ iK)) => [ff sf tf]; rewrite /y; Wtac. rewrite (inl_can_fun_ev aI yiE);apply/(inl_class_eq_bis) => //. exists a; aw;split; fprops. by apply: inl_prop1. by aw; rewrite inl_prop5. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)