proposition: Lemma inl_Lemma5_1ii S i X: inc i (isI S) -> sub X (Vg (isE S) i) -> finite_set X -> constant_fun_on (inl_can_fun S i) X -> exists2 j, gle (isr S) i j & constant_fun_on (Vg (isf S) (J i j)) X.
proof: Proof. move => iI ha hb hc. case: (emptyset_dichot X). by move => ->; exists i; [apply: (inl_prop1 iI) | move => x y /in_set0]. move => neX. have [eqv seqv]:=(inl_equiv_esr S). have ra: forall x y, inc x X -> inc y X -> exists2 k, gle (isr S) i k & Vf (Vg (isf S) (J i k)) x = Vf (Vg (isf S) (J i k)) y. move => x y xX yX; move: (hc _ _ xX yX). rewrite (inl_can_fun_ev iI (ha _ xX)) (inl_can_fun_ev iI (ha _ yX)). move/(inl_class_eq_bis iI iI (ha _ xX) (ha _ yX)) => [k []]. by aw => lik svk; exists k. pose M p := fun k => gle (isr S) i k /\ Vf (Vg (isf S) (J i k)) (P p) = Vf (Vg (isf S) (J i k)) (Q p). pose C p := choose (M p). have rb: forall p, inc p (coarse X) -> M p (C p). move => p /setX_P [pp p1 p2]; apply:choose_pr. by move:(ra _ _ p1 p2) => [k ka kb]; exists k. have rc: forall p, inc p (coarse X) -> inc (C p) (isI S). by move => p/rb [/arg2_sr]; rewrite is_substrate_r. set IK := fun_image (coarse X) C. set x1 := (J (rep X) (rep X)). have x1C : inc x1 (coarse X) by apply:setXp_i; apply: rep_i. have cx1_IK: inc (C x1) IK by apply:funI_i. have neik: nonempty IK by ex_tac. have fsk: finite_set IK by apply: finite_fun_image; apply: finite_prod2. have sik: sub IK (isI S) by move => t/ funI_P [z zK ->]; apply: rc. move: (finite_preorder_directed_bounded (is_preorder_r S) (is_substrate_r S) (@is_directed_r S) neik fsk sik) => [a aI ap]. move: (proj33 (is_preorder_r S) _ _ _ (proj1 (rb _ x1C)) (ap _ cx1_IK)) => lia. exists a => // x y xX yX. move: (setXp_i xX yX) => pc. have C_IK: inc (C (J x y)) IK by apply:funI_i. case:(rb _ pc); aw => ca cb. have cc := (ap _ C_IK). by rewrite -(inl_prop3 ca cc (ha _ xX)) -(inl_prop3 ca cc (ha _ yX)) cb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)