Prob Comp bool Bias Advantage bind uniform Bool eq bool Dist Advantage

lemma ProbComp.boolBiasAdvantage_bind_uniformBool_eq_boolDistAdvantage    {α : Type} (pref : ProbComp α) (real rand : α → ProbComp Bool) :    (do      let a ← pref      let b ← ($ᵗ Bool)      let z ← if b then real a else rand a      pure (b == z)).boolBiasAdvantage =    (do      let a ← pref      real a).boolDistAdvantage      (do        let a ← pref        rand a) := by  let game : ProbComp Bool := do    let a ← pref    let b ← ($ᵗ Bool)    let z ← if b then real a else rand a    pure (b == z)  let left : ProbComp Bool := do    let a ← pref    real a  let right : ProbComp Bool := do    let a ← pref    rand a  let branchGame : ProbComp Bool := do    let b ← ($ᵗ Bool)    let z ← if b then left else right    pure (b == z)  have hbranch : 𝒟[game] = 𝒟[branchGame] := by    apply evalDist_ext    intro x    calc      Pr[= x | game] =          Pr[= x | do            let b ← ($ᵗ Bool)            let a ← pref            let z ← if b then real a else rand a            pure (b == z)] := by              simpa [game, monad_norm] using                (probOutput_bind_bind_swap pref ($ᵗ Bool)                  (fun a b => do                    let z ← if b then real a else rand a                    pure (b == z))                  x)      _ = Pr[= x | branchGame] := by            refine probOutput_bind_congr' ($ᵗ Bool) x ?_            intro b            cases b <;> simp [left, right]  rw [show game.boolBiasAdvantage = branchGame.boolBiasAdvantage by    unfold ProbComp.boolBiasAdvantage    rw [evalDist_ext_iff.mp hbranch true, evalDist_ext_iff.mp hbranch false]]  simpa [branchGame, left, right] using    ProbComp.boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch left right