proposition: Lemma CantorBernstein_eff A B f g: injection_prop f A B -> injection_prop g B A -> bijection_prop (cantor_bernstein_bij A B f g) A B.
proof: Proof. move => [[ff finj] sf tf] [[fg ginj] sg tg]. have ha x: inc x A -> inc (Vf f x) B by move => h; Wtac. have hb x: inc x B -> inc (Vf g x) A by move => h; Wtac. rewrite /cantor_bernstein_bij. set C := A -s Imf g. set Z := Zo _ _. set F := intersection Z. have sCA: sub C A by move => x/setC_P []. pose stable x := forall t, inc t x -> inc (Vf g (Vf f t)) x. have stableA: stable A by move => t te; fprops. have iAZ: inc A Z by apply: (Zo_i (setP_Ti A)). have neZ: nonempty Z by ex_tac. have sCF: sub C F by move => t ta; apply/(setI_P neZ) => u /Zo_hi/proj2; apply. have sgE: sub F A by move => t tF; apply:(setI_hi tF iAZ). have stableF: stable F. move => t tG; apply /(setI_P neZ) => u uz; move:(setI_hi tG uz) => tu. by move/Zo_hi: uz => /proj1; apply. have Ha y : inc y B -> ~ inc (Vf g y) C. move => yF/setC_P [_]; case; apply:(Imf_i fg); ue. have Hb x: inc x F -> inc x C \/ exists2 y, inc y F & x = (Vf g (Vf f y)). move => xG; case: (inc_or_not x C) => xA; [by left | right]. pose D := F -s1 x. case: (all_exists_dichot1 (fun x => inc (Vf g (Vf f x)) D) D) => sB. have BZ: inc D Z. apply:Zo_i; first by apply/setP_P => t /setC1_P [/sgE]. split => // t tA; move: (sCF _ tA) => tG; apply/setC1_P; split => // ee. by case: xA; rewrite - ee. by case/setC1_1: (setI_hi xG BZ). move: sB =>[y /setC1_P [yG yx]] /setC1_P h. case: (equal_or_not x (Vf g (Vf f y))) => xv. by exists y=> //; apply: sAG. by case: h; split; [ apply: (stableF y yG) | apply:nesym]. rewrite sg in ginj; rewrite sf in finj. have Hc y: inc y B -> ~inc y (Imf f) -> ~ inc (Vf g y) F. move => yF ti /Hb; case; first by apply: Ha. move => [x /sgE xE]; move/(ginj _ _ yF (ha _ xE)) => yv. case: ti; rewrite yv; apply: (Imf_i ff); ue. pose gi x:= (union (Vfi1 g x)). have gip x: inc x B -> gi (Vf g x) = x. move => xE; rewrite /gi. suff: (Vfi1 g (Vf g x)) = singleton x by move ->; rewrite setU_1. apply: set1_pr; first by apply:(iim_fun_set1_i fg) => //; ue. move => t ta; move/ (iim_fun_set1_P (Vf g x) fg): ta => [tsf eq1]. apply: ginj => //; ue. have gip2 x: inc x (Imf g) -> inc (gi x) B /\ Vf g (gi x) = x. by move /(Imf_P fg) =>[u usg ->]; rewrite sg in usg; rewrite (gip _ usg). have Pc x: inc x A -> ~inc x F -> inc x (Imf g). by move => xE xG; ex_middle bad; case: xG; apply: sCF; apply/setC_P. set h := fun _ => _. have hf x: inc x F -> h x = Vf f x by move => xG; rewrite/h; Ytac0. have hc x: inc x A -> ~(inc x (Imf g)) -> h x = Vf f x. by move => pa pb; rewrite /h Y_true //; apply: sCF; apply/setC_P. have hd x: inc x A -> inc (h x) B. move => cE; rewrite /h; Ytac xi; first by apply: ha. exact: (proj1(gip2 _ (Pc x cE xi))). have he x: inc x A -> ~inc x F -> inc (h x) B /\ Vf g (h x) = x. move => qa qb; move: (Pc x qa qb) => xg; move: (gip2 x xg) =>[qc qd]. by rewrite /h; Ytac0. saw; apply: lf_bijective => //. move => u v uE vE sh. case: (inc_or_not u F) => uG;case: (inc_or_not v F) => vG. + by move: sh; rewrite /h; Ytac0; Ytac0; apply: finj. + by move: (stableF u uG); rewrite - (hf u uG) sh (proj2 (he _ vE vG)). + by move: (stableF v vG); rewrite - (hf v vG) - sh (proj2 (he _ uE uG)). + by rewrite - (proj2 (he _ uE uG)) - (proj2 (he _ vE vG)) sh. move => y yF. move: (hb y yF); set x := Vf g y => xE. case: (inc_or_not y (Imf f)) => yi; last first. have yG: ~ inc (Vf g y) F. case/Hb; first by apply: Ha. move => [z /sgE zE]; move/(ginj _ _ yF (ha _ zE)) => yv. case: yi; rewrite yv; apply: (Imf_i ff); ue. by ex_tac; rewrite /h (Y_false yG);rewrite -/(gi _) (gip y yF). move/(Imf_P ff): (yi) =>[z zE zv]; rewrite sf in zE. case: (inc_or_not z F) => zG. by exists z => //; rewrite /h (Y_true zG). exists x => //; rewrite /h -/(gi _) (gip y yF) (Y_false) // /x zv => /Hb. move: (ha z zE) => zF; case; first by apply: Ha. move =>[t tG]; move: (sgE t tG)=> tE; move/(ginj _ _ zF (ha _ tE)). by move/(finj _ _ zE tE) => xy; case zG; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)