Pr add split by complement

theorem Pr_add_split_by_complement {α : Type} (D : PMF α)    (f g : α → Prop) :    Pr_{ let r ← D }[ f r ] =    (D >>= (fun r => pure (g r ∧ f r))) True + Pr_{ let r ← D }[ ¬(g r) ∧ f r ] := by  classical  -- 1. Unroll all three probability statements into their tsum forms  rw [prob_tsum_form_singleton D f]  rw [prob_tsum_form_singleton D (fun r => g r ∧ f r)]  rw [prob_tsum_form_singleton D (fun r => ¬(g r) ∧ f r)]  -- 2. Combine the two sums on the RHS using ENNReal.tsum_add  -- Need to prove summability for both, which is true in ENNReal  rw [← ENNReal.tsum_add]  congr 1  funext r  rw [←mul_add]  congr 1  by_cases hg : g r  · simp only [hg, true_and, not_true_eq_false, false_and, ↓reduceIte, add_zero]  · simp only [hg, false_and, ↓reduceIte, not_false_eq_true, true_and, zero_add]