Theorem: SciLean.Prob.ite.arg_te.distribFwdDeriv_rule (SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean)

State before:
W : Type u_1
inst✝¹² : NormedAddCommGroup W
inst✝¹¹ : NormedSpace ℝ W
inst✝¹⁰ : CompleteSpace W
X : Type u_2
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : CompleteSpace X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.40686
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
x dx : X
c : Prop
inst✝ : Decidable c
t e : X → Distribution Y
φ : Y → W × W
⊢ ⟪distribFwdDeriv (fun x => if c then t x else e x) x dx, φ⟫ =
    if c then ⟪distribFwdDeriv t x dx, φ⟫ else ⟪distribFwdDeriv e x dx, φ⟫
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✝¹⁰ : CompleteSpace W
X : Type u_2
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : CompleteSpace X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.40686
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
x dx : X
c : Prop
inst✝ : Decidable c
t e : X → Distribution Y
φ : Y → W × W
h : c
⊢ ⟪distribFwdDeriv (fun x => if c then t x else e x) x dx, φ⟫ =
    if c then ⟪distribFwdDeriv t x dx, φ⟫ else ⟪distribFwdDeriv e x dx, φ⟫
Tactic:
simp[h]
State after:
no goals

State before:
W : Type u_1
inst✝¹² : NormedAddCommGroup W
inst✝¹¹ : NormedSpace ℝ W
inst✝¹⁰ : CompleteSpace W
X : Type u_2
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : CompleteSpace X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.40686
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
x dx : X
c : Prop
inst✝ : Decidable c
t e : X → Distribution Y
φ : Y → W × W
h : ¬c
⊢ ⟪distribFwdDeriv (fun x => if c then t x else e x) x dx, φ⟫ =
    if c then ⟪distribFwdDeriv t x dx, φ⟫ else ⟪distribFwdDeriv e x dx, φ⟫
Tactic:
simp[h]
State after:
no goals