proposition: Lemma Exercise3_1 E F f g: function_prop f E F -> function_prop g F E -> injection f -> exists A A', [/\ sub A E, sub A' F, Vfs f A = A' & Vfs g (F -s A') = E -s A].
proof: Proof. move=> [ff sf tf] [fg sg tg] [_ injf]. rewrite - sg -tg. set R := (source g) -s (Vfs f (target g)). pose p M:= [/\ sub M (source g), sub R M & forall x, inc x M -> inc (Vf f (Vf g x)) M]. have pE: p (source g). split => //; first by rewrite /R; apply: sub_setC. move => x xE; rewrite sg -tf; Wtac. rewrite sf -tg; apply: Vf_target => //. set Z:= Zo (\Po (source g)) p. have EZ: inc (source g) Z by apply: Zo_i; aw;trivial;apply: setP_Ti. have neZ: nonempty Z by exists (source g). set B':= intersection Z; set B := Vfs g B'. have p1: sub R B'. by move=> t tR; apply: setI_i => // y /Zo_hi [_ p1 _]; apply: p1. have p2: forall x, inc x B' -> inc (Vf f (Vf g x)) B'. move => x xB'; apply: setI_i => // y yZ; move: (yZ) => /Zo_P. by move => [ _ [_ _]]; apply; apply: setI_hi yZ. have sBF: sub B' (source g) by apply: (setI_s1 EZ). have aux:sub (target g) (source f) by rewrite sf -tg; fprops. have p3:forall x, inc x B' -> inc x R \/ exists2 y, inc y B' & x= (Vf f (Vf g y)). move=> x xB'; case: (inc_or_not x R) => xR; first by left. have xsg: inc x (source g) by apply: sBF. case: (inc_or_not x (Vfs f (target g))); last first. move => h; case: xR; apply /setC_P;split => //. move=> /(Vf_image_P ff aux) [u [utg Wu]]. set C := B' -s1 x; case: (inc_or_not C Z) => CZ. by move: (setI_hi xB' CZ)=> /setC_P [_] /set1_P. have pA: sub C (source g). by apply: (@sub_trans B') =>//; apply: sub_setC. have pB: inc C (\Po (source g)) by apply /setP_P. have pC:sub R C by move => t tR; apply/setC1_P;split;fprops=> tx;case: xR; ue. right; ex_middle hyp. case: CZ; apply /Zo_P;split => //; split => //; move => v /setC1_P [vB' vx]. apply /setC1_P;split; [by apply: p2 | move=> aux2; case: hyp; ex_tac]. have sBE: sub B (target g). move => t /(Vf_image_P fg sBF) [u uA ->]; Wtac. set A':= (source g) -s B'. have AF: sub A' (source g) by apply: sub_setC. set A := (target g) -s B. have AE: sub A (target g) by apply: sub_setC. exists A; exists A'; split => //; last by rewrite /A' /A !setC_K //. rewrite /A/A'. rewrite tg - sf in AE. set_extens t. move /(Vf_image_P ff AE)=> [u] /setC_P [utf hh] ->; apply /setC_P;split => //. rewrite sg -tf; Wtac. dneg Wa; case: (p3 _ Wa). move => /setC_P [_] /(Vf_image_P ff aux); case; ex_tac. move=> [y yB' ww]. have wF: inc (Vf g y) (target g) by apply: Vf_target => //; apply: sBF. rewrite tg - sf in utf wF;rewrite (injf _ _ utf wF ww). apply /(Vf_image_P fg sBF); ex_tac. move => /setC_P[tsf ntA]. case: (inc_or_not t R) => tR; first by case: ntA; apply: p1. have dn: forall (P Q: Prop), P -> ~ (P /\ ~ Q) -> Q. move=> P Q nP npq; case: (p_or_not_p Q) => nQ //;case: npq;split => //. move: tR => /setC_P => aux2; move: (dn _ _ tsf aux2). move=> /(Vf_image_P ff aux) [u usg Wu]; case: (inc_or_not u B) => uB. move: uB => /(Vf_image_P fg sBF) [v vA Wv]; case: ntA. by rewrite Wu Wv; apply: p2. apply /(Vf_image_P ff AE); exists u => //; apply /setC_P;split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)