Theorem: Probly.ite.arg_tf.randFwdDeriv_rule (Probly/RandFwdDeriv.lean)

State before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.14943
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.15060
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.15177
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.15300
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
⊢ (randFwdDeriv fun w => if c then t w else f w) = fun w dw => if c then randFwdDeriv t w dw else randFwdDeriv f w dw
Tactic:
if h : c then simp[h] else simp[h]
State after:
no goals

State before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.14943
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.15060
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.15177
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.15300
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
h : c
⊢ (randFwdDeriv fun w => if c then t w else f w) = fun w dw => if c then randFwdDeriv t w dw else randFwdDeriv f w dw
Tactic:
simp[h]
State after:
no goals

State before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.14943
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.15060
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.15177
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.15300
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
h : ¬c
⊢ (randFwdDeriv fun w => if c then t w else f w) = fun w dw => if c then randFwdDeriv t w dw else randFwdDeriv f w dw
Tactic:
simp[h]
State after:
no goals