Theorem: Probly.ite.arg_tf.randDeriv_rule (Probly/RandDeriv.lean)

State before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
⊢ (randDeriv fun w => if c then t w else f w) = fun w dw => if c then randDeriv t w dw else randDeriv f w dw
Tactic:
funext w dw
State after:
case h.h
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw

State before:
case h.h
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv 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.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
h : c
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv 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.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
h : ¬c
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw
Tactic:
simp [h]
State after:
no goals