Exp eq cexp add cexp

lemma exp_eq_cexp_add_cexp (q : α → Prop) :    f.exp u = f.cexp u q * f.pr q + f.cexp u (λ x ↦ ¬q x) * (1 - f.pr q) := by  by_cases q0 : f.pr q = 0  · simp only [cexp, q0, div_zero, sub_zero, mul_zero, zero_add, pr_neg, div_one, mul_one]    simp only [pr_eq_zero] at q0; apply exp_congr; intro x m    simp only [q0 x m, not_false_eq_true, ↓reduceIte]  by_cases q1 : f.pr q = 1  · simp only [cexp, q1, div_one, mul_one, sub_self, mul_zero, add_zero]    simp only [pr_eq_one] at q1; apply exp_congr; intro x m; simp only [q1 x m, if_true, and_true]  replace q1 : 1 - f.pr q ≠ 0 := by rw [sub_ne_zero]; exact Ne.symm q1  simp only [cexp, pr_neg, div_mul_cancel₀ _ q0, div_mul_cancel₀ _ q1]  simp only [pr, ←exp_add]; apply exp_congr; intro x _  by_cases qx : q x; repeat { simp only [qx, if_true, if_false]; norm_num }