proposition: Lemma exercise3_10 f g h: function f -> function g -> function h-> source g = target f -> source h = target g -> source f = target h -> injection (h \co (g \co f)) -> surjection (g \co (f \co h)) -> (injection (f \co (h \co g)) \/ surjection (f \co (h \co g))) -> [/\ bijection f, bijection g & bijection h].
proof: Proof. move=> ff fg fh sgtf shtg sfth ihgf sgfh is_fgh. have cfh: f \coP h by []. have chg: h \coP g by []. have cgf: g \coP f by []. rewrite compfA // in ihgf. have fhg: function (h \co g) by fct_tac. have chgf: (h \co g) \coP f by hnf; aw. move: (right_compose_fi chgf ihgf) => inf. have ffh: function (f \co h) by fct_tac. have cgfh: g \coP (f \co h) by hnf; aw. move: (left_compose_fs cgfh sgfh) => sg. case is_fgh. rewrite compfA// => ifhg. have cfhg: (f \co h) \coP g by hnf; aw. move: (right_compose_fi cfhg ifhg) => ig. move: (left_compose_fs2 cgfh sgfh ig)=> sfh. move: (left_compose_fs cfh sfh) =>sf. move: (left_compose_fi2 cfhg ifhg sg) => ifh. have bfh: (bijection (f \co h)) by []. have bf: (bijection f) by []. have bg: (bijection g) by []. move: (right_compose_fb cfh bfh bf). done. move=> sfhg. have cfhg: (f \coP (h \co g)) by hnf; aw. move: (left_compose_fs cfhg sfhg) => sf. have bf: (bijection f) by []. move: (left_compose_fs2 cfhg sfhg inf) => shg. move:(left_compose_fi2 chgf ihgf sf) => ihg. move: (right_compose_fi chg ihg) => ig. have bg: (bijection g) by []. have bhg: (bijection (h \co g)) by []. move: (left_compose_fb chg bhg bg). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)