proposition: Lemma Exercise4_6k E F A G: finite_set F -> sub G F -> (forall x, inc x E -> sub (A x) F) -> E46b_conc E A -> E46c_conc E A G -> E46b_hyp E F A.
proof: Proof. move=> fsF GF Ap h1 h2. set Gi:= G *s1 C0. set Fi:= F *s1 C1. set Ei:= E *s1 C2. set Et := Gi \cup (Fi \cup Ei). have Gp1: forall x, inc x G -> inc (J x C0) Et. by move=> x xG; apply /setU2_P;left; apply:indexed_pi. have Fp1: forall x, inc x F -> inc (J x C1) Et. by move=> x xG; apply /setU2_P;right; apply /setU2_P;left; apply:indexed_pi. have Ep1: forall x, inc x E -> inc (J x C2) Et. by move=> x xG;apply /setU2_P;right; apply /setU2_P;right; apply:indexed_pi. pose rc x y := [\/ x = y, [/\ Q x = C0, Q y = C1 & P x = P y] | [/\ (Q x = C0 \/ Q x = C1), Q y = C2 & inc (P x) (A (P y))]]. set r := graph_on rc Et. have sr: substrate r = Et by apply: graph_on_sr; move=> a _; in_TP4. have rvP: forall x y, gle r x y <-> [/\ inc x Et, inc y Et & rc x y]. by move=> x y; apply /graph_on_P1. move: C0_ne_C1 C2_ne_C01 => n01 [n20 n21]. have trr: transitive_r rc. move => x y z xy; case: (xy); first by move=> ->. move=> aux; case; first by move=> <-. by move: aux => [_ pa _] [pb _ _]; case: n01; rewrite - pa - pb. move => [a2 pa pb]; case: a2. by move => a2; case: n01; rewrite -a2; move : aux => [_ -> _]. by move: aux => [pc pd pe] h; constructor 3; rewrite pe; split => //; left. move=> [pa pb pc]; case; first by move => <-. by move => [pd _ _]; case: n20; rewrite -pb -pd. by rewrite pb;move => [pd _ _];case: pd => pd; [ case: n20 | case: n21]. have arr: antisymmetric_r rc. move => x y xy; case: xy; first by move=> ->. move=> aux; case; first by move=> <-. by move: aux => [_ pa _] [pb _ _]; case: n01; rewrite - pa - pb. by move: aux => [pa _ _] [_ pb _]; case: n20; rewrite - pa - pb. move=> [_ pb _]; case; first by move => <-. by move => [pd _ _]; case: n20; rewrite -pb -pd. by rewrite pb;move => [pd _ _];case: pd => pd; [ case: n20 | case: n21]. have or: order r. apply: order_from_rel;split => //. by move=> x y _; split; constructor 1. set m := cardinal F. have pa: (exists2 x, inc x (free_subsets r) & cardinal x = m). exists Fi; last by rewrite (cardinal_indexed F C1). apply: Zo_i; first by apply /setP_P; rewrite sr /Et => t; fprops. move=> x y xFi yFi; move: xFi yFi=> /indexed_P [_ _ qx] /indexed_P [_ _ qy]. move /rvP => [_ _]; case => //. by move=> [qxa _]; case: n01; rewrite -qx -qxa. by move=> [_ qya _]; case: n21; rewrite -qy -qya. have pb: forall x, inc x Et -> pairp x. by move => x;case /setU2_P; [ | case /setU2_P]; move/indexed_P => []. have pc: order_width r m. split => // x0 => /Zo_P [] /setP_P; rewrite sr; move=> xET x0f. pose f x := Yo (Q x = C0) (J (P x) C1) x. set x1 := fun_image x0 f. have x1E: sub x1 Et. rewrite /x1; move=> t /funI_P [z zx0 ->]. move: (xET _ zx0) => zEt; rewrite /f; Ytac zza => //;apply: Fp1. move: (zEt); case /setU2_P. by move /indexed_P => [_ hh _]; apply: GF. by case /setU2_P;move/indexed_P => [_ h3 h4]//;case: n20;rewrite -h4 - zza. have x1f: free_subset r x1. move=> x y /funI_P [u ux0 ->] /funI_P [v vx0 ->] h. case: (equal_or_not u v) => nuv; first by rewrite nuv. move: (xET _ ux0)(xET _ vx0) => uEt vEt. move: h;rewrite /f; Ytac uza; Ytac vza. + by move /rvP=> [_ _]; case => //;aw; move => [xx yy]; [case: n01 | case: n21]. + move /rvP => [_ _]; case => //; aw; first by move => [p1]; case: n01. move => [_ aa bb]. case: nuv;apply: (x0f u v ux0 vx0); apply /rvP; split => //. by constructor 3; split => //; left. + by move /rvP => [ _ _]; case => //; aw; move => [aa /esym bb]. + by move=> uv;case: nuv; apply: (x0f u v). have -> : cardinal x0 = cardinal x1. apply /card_eqP; exists (Lf f x0 x1); saw; apply: lf_bijective. move=> t tx0; apply /funI_P; ex_tac. move=> u v ux0 vx0; rewrite /f; Ytac uza; Ytac vza. + move: (pb _ (xET _ ux0)) (pb _ (xET _ vx0)) => xp yp sJ. apply: pair_exten => //; [apply: (pr1_def sJ) | ue ]. + move=> sj; move: (f_equal P sj) (f_equal Q sj); aw => qa qb. by apply: (x0f u v) => //; apply /rvP;split;fprops; constructor 2. + move=> sj; move: (f_equal P sj) (f_equal Q sj); aw => qa qb. by symmetry;apply:(x0f v u)=>//; apply /rvP;split;fprops; constructor 2. + done. by move=> y/funI_P. set H1 := Zo E (fun z => inc (J z C2) x1). set H2 := Zo F (fun z => inc (J z C1) x1). have ->: cardinal x1 = (cardinal H1) +c (cardinal H2). have ->: x1 = (x1 \cap Ei) \cup (x1 \cap Fi). rewrite - (set_IU2r x1 Ei Fi); symmetry; apply /setI2id_Pl. move => t; case /funI_P => [z zx0 ->]. move: (xET _ zx0); case /setU2_P. move /indexed_P => [pz Pz Qz]; apply /setU2_P; right. by rewrite /f; Ytac0; apply: indexed_pi; apply: GF. case /setU2_P; move /indexed_P => [pz Pz Qz]; rewrite /f. rewrite Qz; Ytac0; apply /setU2_P; right; by apply /indexed_P. rewrite Qz; Ytac0; apply /setU2_P; left; by apply /indexed_P. rewrite csum2cl csum2cr. have di: disjoint (x1 \cap Ei) (x1 \cap Fi). by apply: disjoint_pr; move => u /setI2_P [_] /indexed_P [_ _ qc] /setI2_P [_] /indexed_P[_ _ qb]; case: n21; rewrite - qc -qb. rewrite (csum2_pr5 di); apply: csum2_pr2; apply/card_eqP. exists (Lf P (x1 \cap Ei) H1). saw; apply: lf_bijective. - move=> t /setI2_P [tx1] /indexed_P [pt PE Qt]. by apply: Zo_i => //; rewrite -Qt pt. - move=> u v /setI2_P [_] /indexed_P [pt _ Qt] /setI2_P [_] /indexed_P [pv _ Qv]. by move=> aux; apply: pair_exten => //; ue. - move=> y /Zo_P [yE px1]. exists (J y C2); last by aw. by apply/setI2_P;split => //;apply:indexed_pi. exists (Lf P (x1 \cap Fi) H2). saw; apply: lf_bijective. + move=> t /setI2_P [tx1] /indexed_P [pt PE Qt]. by apply: Zo_i => //; rewrite -Qt pt. + move=> u v /setI2_P [_] /indexed_P [pt _ Qt] /setI2_P[_] /indexed_P [pv _ Qv] aux. apply: pair_exten => //; ue. + move=> y =>/Zo_P [yE px1]; exists (J y C1); last by aw. by apply /setI2_P; split => //; apply: indexed_pi. have hE: sub H1 E by apply: Zo_S. move: (h1 _ hE); set K:= (union _). have KM: sub K F. move=> t /setU_P [y ty] /funI_P [z zH1 zh2]. move: zH1 => /Zo_P [zE _]. by move: (Ap _ zE); rewrite - zh2; apply. move: (cardinal_setC KM); rewrite -/m. suff: (sub H2 (F -s K)). move=> s1; move: (sub_smaller s1) => qa qb qc. by rewrite -qb; apply: csum_Mlele. move=> t =>/Zo_P [tF px1]; apply /setC_P;split => //. move=> /setU_P [y ty] /funI_P [z zH1 Az]. move: zH1 => /Zo_P [zE J2x1]. have le1: (gle r (J t C1) (J z C2)). apply /rvP;split;fprops; constructor 3; aw. split => //; [ by right | by rewrite - Az]. by move: (pr2_def (x1f _ _ px1 J2x1 le1))=> h; case:n21. have mN: inc m Nat by move: fsF => /NatP. move: (Exercise4_5d or mN pc) => [X [[[uX deX] neX] cX toeX]]. pose f x := choose (fun z => inc (J x C1) z /\ inc z X). have fp1: forall x, inc x F -> (inc (J x C1) (f x) /\ inc (f x) X). move=> x xF; apply choose_pr;move:(Fp1 _ xF); rewrite - sr -uX;move /setU_P. by move => [t t1 t2]; exists t. have taf: lf_axiom f F X by move => t tF; move: (fp1 _ tF) => [p1 p2]. have bijF: bijection (Lf f F X). apply:bijective_if_same_finite_c_inj;first by rewrite lf_source lf_target cX. by aw. apply: lf_injective => //. move => u v uF vF; move: (fp1 _ uF) (fp1 _ vF) => [p1 p2] [p3 p4] sf. rewrite - sf in p3; move /total_subordersP: (toeX _ p2) => [sfu [orf]]. rewrite iorder_sr // => aux. move: (aux _ _ p1 p3); case => leuv; move: (iorder_gle1 leuv) => /rvP [qa qb]; case => aux1. + exact: (pr1_def aux1). + by move: aux1; aw; move=> [r1 _ _]; case: n01. + by move: aux1; aw; move=> [_ r1 _]; case: n21. + symmetry; exact (pr1_def aux1). + by move: aux1 => [_ _ ]; aw. + by move: aux1; aw; move=> [_ r1 _]; case: n21. pose g x := choose (fun z => inc (J x C2) z /\ inc z X). have gp1: forall x, inc x E -> (inc (J x C2) (g x) /\ inc (g x) X). move=> x xE;apply choose_pr;move: (Ep1 _ xE); rewrite - sr -uX; move/setU_P. by move => [t t1 t2]; exists t. have tag: lf_axiom g E X by move => t tE; move: (gp1 _ tE) => [p1 p2]. have bijG: injection (Lf g E X). apply: lf_injective => //. move => u v uF vF; move: (gp1 _ uF) (gp1 _ vF) => [p1 p2] [p3 p4] sf. rewrite - sf in p3; move/total_subordersP: (toeX _ p2) => [sfu [orf]]. rewrite iorder_sr //. move=> aux; move: (aux _ _ p1 p3); case => leuv; move: (iorder_gle1 leuv) => /rvP [qa qb]; case; aw => aux1. + exact: (pr1_def aux1). + by move: aux1 => [_ _]. + by move: aux1 => [aux2 _ _];case: aux2=> h; [case: n20 | case: n21]. + by rewrite (pr1_def aux1). + by move: aux1 => [_ _ ->]. + by move: aux1 => [aux2 _ _];case: aux2=> h; [case: n20 | case: n21]. set h := compose (inverse_fun (Lf f F X)) (Lf g E X). have sh: source h = E by rewrite /h; aw. have th: target h = F by rewrite /h; aw. move: (inverse_bij_fb bijF) => bif. have cifg: composable (inverse_fun (Lf f F X)) (Lf g E X). by split => //; try fct_tac; aw. have ih: injection h by apply: compose_fi => //; move: bif => [ok _]. have ph: forall x, inc x E -> inc (Vf h x) (A x). move=> x xE; rewrite /h; aw. set y := Vf (inverse_fun (Lf f F X)) (g x). have yF: inc y F. have ->: F = target (inverse_fun (Lf f F X)) by aw. by apply: Vf_target; try fct_tac; aw; apply: tag. move: (fp1 _ yF) (gp1 _ xE) => [p1 p2] [p3 p4]. have aux: inc (g x) (target (Lf f F X)) by aw; apply: tag. move: (inverse_V bijF aux); rewrite -/y LfV // compfV//; aw; bw => //. move=> eq0; rewrite - eq0 in p3; aw. move /total_subordersP: (toeX _ p2) => [sfy [orX]]; rewrite iorder_sr //. move=> aux1; move: (aux1 _ _ p1 p3); case => leuv; move: (iorder_gle1 leuv); move /rvP=> [qa qb]; case => aux2; try (case: n21;move: (pr2_def aux2); fprops); move: aux2; aw. + by move=> [zbc _]; case: n01. + by move=> [_ _]. + by move=> [zba _]; case: n01. + by move=> [_ zbc _]; case: n21. have gp: forall t, inc t G -> inc (J t C0) (f t). move=> t tG; move: (Gp1 _ tG); rewrite - sr -uX => /setU_P [y Jy yX]. move: (fp1 _ (GF _ tG)) => [Jf1 fX]. set z := Vf (inverse_fun (Lf f F X)) y. have zF: inc z F. have ->: F = target (inverse_fun (Lf f F X)) by aw. apply: Vf_target => //; [fct_tac | by aw ]. have: y = Vf (Lf f F X) z by rewrite inverse_V => //; aw. rewrite LfV//; move: (fp1 _ zF) => [p5 p6]. move => yf; rewrite yf in Jy. case: (equal_or_not z t) => zt; first by move: Jy; rewrite zt. move /total_subordersP: (toeX _ p6) => [aux3 [orX]]; rewrite iorder_sr //. move=> aux1; move: (aux1 _ _ Jy p5);case => leuv;move: (iorder_gle1 leuv); move /rvP => [qc qd]; case => aux2. + by case: zt; move: (pr2_def aux2). + by case: zt; move: aux2 => [_ _]; aw. + by case: n21;move: aux2=> [_ e1 _]; move: e1;aw. + by case: zt; move: (pr1_def aux2). + by case: zt; move: aux2 => [_ _]; aw. + by case: n20;move: aux2=> [_ e1 _]; move: e1;aw. by exists h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)