Theorem: SciLean.Rand.ite_pdf (SciLean/Core/Rand/Rand.lean)

State before:
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 μ
Tactic:
if h : c then
  simp [h]
else
  simp [h]
State after:
no goals

State before:
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
h : c
⊢ pdf R (if c then t else e) μ = if c then pdf R t μ else pdf R e μ
Tactic:
simp [h]
State after:
no goals

State before:
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
h : ¬c
⊢ pdf R (if c then t else e) μ = if c then pdf R t μ else pdf R e μ
Tactic:
simp [h]
State after:
no goals