proposition: Lemma exercise6_9 F G p f r: equivalence r -> F = substrate r -> p = canon_proj r -> surjection f -> source f = G -> target f = quotient r -> exists E g h, [/\ surjection_prop g E F, surjection_prop h E G & p \co g = f \co h].
proof: Proof. move=> er sr xr sjf sf tf. have ff: function f by fct_tac. have ba:= C1_ne_C0. set Ea:= F \times (singleton C0). set Eb:= G \times (singleton C1). set E:= Ea \cup Eb. have gE: sgraph E by move => T /setU2_P; case; move /setX_P => [ok _]. have xep: forall x, inc x E -> (Q x = C0 \/ Q x = C1). move=> x /setU2_P; case; move /setX_P => [_ _ ] /set1_P ->; fprops. have xgp:forall x, inc x G -> inc (Vf f x) (quotient r). move=> x xg; rewrite - tf;apply: Vf_target => //; ue. have xgp1:forall x, inc x G -> inc (rep (Vf f x)) F. move=> x xG; rewrite sr;fprops. set (gz :=fun z=> Yo (Q z = C0) (P z) (rep (Vf f (P z)))). have gzP:forall z, inc z Ea -> gz z = P z. move=> z /setX_P [_ _] /set1_P h; rewrite /gz Y_true //. have gzp': forall z, inc z Ea -> inc (gz z) F. by move=> z zEa; rewrite gzP//; move /setX_P : zEa => [_ ok _]. have gzQ:forall z, inc z Eb -> gz z = rep (Vf f (P z)). move=> z/setX_P [_ _] /set1_P => h; rewrite /gz Y_false //; ue. have gzq':forall z, inc z Eb -> inc (gz z) F. by move=> z zE; rewrite gzQ //; apply: xgp1; move /setX_P : zE => [_ ok _]. have tag:lf_axiom gz E F. move=> t; case /setU2_P; [apply: gzp'| apply: gzq']. set (g:= Lf gz E F). have sj: surjection g. rewrite /g;apply: lf_surjective =>//; move=> y yF. have p1: inc (J y C0) Ea by rewrite /Ea; fprops. have p2: inc (J y C0) E by rewrite /E; aw;fprops. by ex_tac; rewrite gzP; aw. have gp: forall x, inc x Eb -> Vf (canon_proj r) (gz x) = Vf f (P x). move=> x xEb. have gzs: inc (gz x) (substrate r) by rewrite - sr; apply: gzq'. have xE: inc x E by move: xEb; rewrite /E;aw => ee; fprops. rewrite canon_proj_V // gzQ //; apply: class_rep=>//; apply: xgp. by move /setX_P : xEb => [_ ok _]. set (ha:= fun x => rep (Vfi1 f (Vf (canon_proj r) x))). have haF:forall x, inc x F -> ha x = rep (Vfi1 f (class r x)). move=> x xF; rewrite /ha canon_proj_V //; ue. have haF':forall x, inc x F -> sub (Vfi1 f (class r x)) G. move=> x xF t /iim_graph_P [u _ jg]; rewrite - sf; Wtac. have haF'': forall x, inc x F -> inc (ha x) (Vfi1 f (class r x)). move => x xF; rewrite haF //; apply: rep_i. have ct: inc (class r x) (target f) by rewrite tf; rewrite sr in xF; fprops. move:((proj2 sjf) _ ct)=> [u us]; move => ->. exists u; apply /iim_graph_P; ex_tac; apply: Vf_pr3=>//. have haG: forall x, inc x F -> inc (ha x) G. by move=> x xF; apply: (haF' _ xF); apply: haF''. set(hz:= fun z=> Yo (Q z = C0) (ha (P z)) (P z)). have hzG: forall z, inc z E -> inc (hz z) G. rewrite /hz;move=> z /setU2_P [] /setX_P [_ pa] /set1_P ->; Ytac0 => //. by apply: haG. set(h:=Lf hz E G). have sh: surjection h. rewrite /h;apply: lf_surjective=>// y yG. have JEb:inc (J y C1) Eb by rewrite /Eb;aw; fprops. have JE: (inc (J y C1) E) by rewrite /E; aw; fprops. by ex_tac; rewrite /hz; aw; rewrite Y_false. have WWh: forall x, inc x Ea -> Vf f (hz x) = Vf (canon_proj r) (P x). move=> x xEa. have xE: inc x E by rewrite /E; aw; intuition auto with fprops. have Ps: inc (P x) (substrate r) by rewrite - sr -gzP//; apply: gzp'. rewrite /hz canon_proj_V//. move /setX_P: xEa=> [px PF] /set1_P ->; Ytac0. move /iim_graph_P: (haF'' _ PF) => [u ] /set1_P <- Jg; Wtac. exists E; exists g; exists h; rewrite /surjection_prop/g/h;aw;split => //. have cpg: p \coP g. split; first by rewrite xr;apply: canon_proj_f. by fct_tac. rewrite xr /g; aw; ue. have cfh: composable f h by split => //; try fct_tac; rewrite /h; aw. have sg: source g = source h by rewrite /g/h; aw. have tp: target p = target f by rewrite xr; aw. move: sj => [fg _]. apply: function_exten; try fct_tac; aw; trivial. move=> x xE /=; rewrite ! compfV // ? lf_source // !LfV // . move /setU2_P: (xE) => [] xE'. have Ps: inc (P x) (substrate r) by rewrite - sr -gzP //; apply: gzp'. by rewrite WWh // /g; aw; trivial; rewrite gzP // xr; aw. rewrite xr gp /h /hz; aw =>//; rewrite Y_false //. by move /setX_P: xE'=> [_ _ ] /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)