proposition: Lemma reasoning_by_cases (U : finType) (P : {fdist U}) (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}) E : `Pr[ X \in E ] = \sum_(b <- fin_img Y) `Pr[ [% X, Y] \in (E `* [set b])].
proof: Proof. rewrite pr_eq_setE. have -> : X @^-1: E = \bigcup_d [% X, Y] @^-1: ((E `* [set d])). rewrite bigcup_preimset; apply/setP => u; rewrite !inE; apply/idP/bigcupP. by move=> XuE; exists (Y u) => //; rewrite !inE /= XuE /=. by case=> b _; rewrite !inE => /andP[] ->. rewrite bigcup_preimset /Pr partition_big_preimset /=. rewrite partition_disjoint_bigcup /=; last first. move=> i j ij; rewrite -setI_eq0; apply/eqP/setP => u; rewrite !inE. by apply/negbTE/negP=> /andP[] /andP[] -> /eqP -> /=; move/negP: ij; exact. apply/esym; set F := BIG_F. transitivity (\sum_(b in B) F b). rewrite [in RHS](bigID (mem (fin_img Y))) /=. rewrite [X in _ = _ + X]big1 ?addR0 //. by rewrite big_uniq // undup_uniq. by move=> b bY; rewrite {}/F pr_in_pairC pr_in_domin_RV2 // pr_eq_set1 pr_eq0. by apply eq_bigr => b _; rewrite /F pr_eq_setE /Pr partition_big_preimset. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist