Theorem: SciLean.Prob.ite.arg_tf.randDeriv_rule (SciLean/Modules/Prob/RandDeriv.lean)

State before:
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
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
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
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
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
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:
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
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:
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
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