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

State before:
R : Type
inst✝¹ : RealScalar R
inst✝ : MeasureSpace R
θ θ' : R
⊢ pdf R (flip θ) (flip θ').ℙ = fun b => if b = true then θ / θ' else (1 - θ) / (1 - θ')
Tactic:
sorry_proof
State after:
no goals