Theorem: SciLean.Rand.flip.pdf (SciLean/Core/Rand/Distributions/Flip.lean)

State before:
R : Type
inst✝¹ : RealScalar R
inst✝ : MeasureSpace R
x : R
⊢ Rand.pdf R (flip x) Measure.count = fun b =>
    let x := (x ⊔ 0) ⊓ 1;
    if b = true then x else 1 - x
Tactic:
sorry_proof
State after:
no goals