Theorem: Probly.ite_push_fdE (Probly/PushPullE.lean)

State before:
X : Type
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : MeasurableSpace X
Y : Type
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : MeasurableSpace Y
Z : Type ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
Tactic:
if h : c then simp[h] else simp[h]
State after:
no goals

State before:
X : Type
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : MeasurableSpace X
Y : Type
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : MeasurableSpace Y
Z : Type ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
h : c
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
Tactic:
simp[h]
State after:
no goals

State before:
X : Type
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : MeasurableSpace X
Y : Type
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : MeasurableSpace Y
Z : Type ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
h : ¬c
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
Tactic:
simp[h]
State after:
no goals