SPMF bool Bias Advantage eq bool Dist Advantage coin branch

lemma SPMF.boolBiasAdvantage_eq_boolDistAdvantage_coin_branch    (coin p q : SPMF Bool)    (hcoin_true : Pr[= true | coin] = 1 / 2)    (hcoin_false : Pr[= false | coin] = 1 / 2)    (hp : Pr[= true | p] + Pr[= false | p] = 1)    (hq : Pr[= true | q] + Pr[= false | q] = 1) :    (coin >>= fun b =>      (if b then p else q) >>= fun z => pure (b == z)).boolBiasAdvantage =    p.boolDistAdvantage q := by  have hbt : ∀ x : Bool,      Pr[= x | (if (true : Bool) then p else q) >>= fun z =>        (pure (true == z) : SPMF Bool)] = Pr[= x | p] := by    intro x; cases x <;> simp  have hbf : ∀ x : Bool,      Pr[= x | (if (false : Bool) then p else q) >>= fun z =>        (pure (false == z) : SPMF Bool)] = Pr[= (!x) | q] := by    intro x; cases x <;> simp  have hgame : ∀ x : Bool, Pr[= x | coin >>= fun b =>      (if b then p else q) >>= fun z => pure (b == z)] =    (Pr[= x | p] + Pr[= (!x) | q]) / 2 := fun x => by    rw [probOutput_bind_eq_tsum, tsum_fintype (L := .unconditional _), Fintype.sum_bool,      hcoin_true, hcoin_false, hbt x, hbf x, ← left_distrib, one_div, mul_comm, div_eq_mul_inv]  have htotal : Pr[= true | coin >>= fun b =>      (if b then p else q) >>= fun z => pure (b == z)] +    Pr[= false | coin >>= fun b =>      (if b then p else q) >>= fun z => pure (b == z)] = 1 := by    rw [hgame true, hgame false]    simp only [Bool.not_true, Bool.not_false, ENNReal.div_add_div_same]    rw [show Pr[= true | p] + Pr[= false | q] + (Pr[= false | p] + Pr[= true | q]) =        (Pr[= true | p] + Pr[= false | p]) + (Pr[= true | q] + Pr[= false | q]) from by ring,      hp, hq, show (1 : ℝ≥0∞) + 1 = 2 from by norm_num]    exact ENNReal.div_self (by positivity) ENNReal.ofNat_ne_top  rw [SPMF.boolBiasAdvantage_eq_two_mul_abs_sub_half _ htotal, hgame true, Bool.not_true]  rw [show Pr[= false | q] = 1 - Pr[= true | q] from by      rw [← hq, ENNReal.add_sub_cancel_left probOutput_ne_top],    ENNReal.toReal_div, ENNReal.toReal_add probOutput_ne_top      (ENNReal.sub_ne_top ENNReal.one_ne_top),    ENNReal.toReal_sub_of_le (by rw [← hq]; exact le_add_right (le_refl _)) ENNReal.one_ne_top,    ENNReal.toReal_one, ENNReal.toReal_ofNat]  unfold SPMF.boolDistAdvantage  rw [show ((Pr[= true | p]).toReal + (1 - (Pr[= true | q]).toReal)) / 2 - 1 / 2 =      ((Pr[= true | p]).toReal - (Pr[= true | q]).toReal) / 2 from by ring, abs_div, abs_two,    mul_div_cancel₀ _ two_ne_zero]