Theorem: SciLean.Rand.ite_pull_E (SciLean/Core/Rand/PushPullExpectation.lean)

State before:
R : Type ?u.8434
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.9646
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ ψ : X → Y
⊢ (if c then t.𝔼 φ else e.𝔼 ψ) = (if c then t else e).𝔼 (if c then φ else ψ)
Tactic:
if h : c then simp[h] else simp[h]
State after:
no goals

State before:
R : Type ?u.8434
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.9646
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ ψ : X → Y
h : c
⊢ (if c then t.𝔼 φ else e.𝔼 ψ) = (if c then t else e).𝔼 (if c then φ else ψ)
Tactic:
simp[h]
State after:
no goals

State before:
R : Type ?u.8434
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.9646
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ ψ : X → Y
h : ¬c
⊢ (if c then t.𝔼 φ else e.𝔼 ψ) = (if c then t else e).𝔼 (if c then φ else ψ)
Tactic:
simp[h]
State after:
no goals