Theorem: SciLean.Rand.uniformI.pdf (SciLean/Core/Rand/Distributions/UniformI.lean)

State before:
R : Type
inst✝¹ : RealScalar R
inst✝ : MeasureSpace R
⊢ Rand.pdf R (uniformI R) volume = fun x => if 0 < x ∧ x < 1 then 1 else 0
Tactic:
sorry_proof
State after:
no goals