if h : c then
  simp [h]
else
  simp [h]
X : Type
Y : Type ?u.127136
Z : Type ?u.127139
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
R : Type u_1
inst✝³ : RealScalar R
inst✝² : MeasurableSpace X
inst✝¹ : MeasurableSpace Y
c : Prop
inst✝ : Decidable c
t e : Rand X
μ : Measure X
⊢ pdf R (if c then t else e) μ = if c then pdf R t μ else pdf R e μ
no goals