Theorem: Probly.uniform.arg_ab.randFwdDeriv_rule (Probly/Uniform.lean)

State before:
a✝ b✝ : ℝ
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.2943
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3060
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3177
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3294
inst✝¹ : MeasurableSpace α
β : Type ?u.3300
inst✝ : MeasurableSpace β
a b : W → ℝ
ha : Differentiable ℝ a
hb : Differentiable ℝ b
⊢ (randFwdDeriv fun w => uniform (a w) (b w)) = fun w dw =>
    let ada := fwdDeriv ℝ a w dw;
    let bdb := fwdDeriv ℝ b w dw;
    fduniform ada.1 bdb.1 ada.2 bdb.2
Tactic:
funext w dw
State after:
case h.h
a✝ b✝ : ℝ
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.2943
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3060
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3177
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3294
inst✝¹ : MeasurableSpace α
β : Type ?u.3300
inst✝ : MeasurableSpace β
a b : W → ℝ
ha : Differentiable ℝ a
hb : Differentiable ℝ b
w dw : W
⊢ randFwdDeriv (fun w => uniform (a w) (b w)) w dw =
    let ada := fwdDeriv ℝ a w dw;
    let bdb := fwdDeriv ℝ b w dw;
    fduniform ada.1 bdb.1 ada.2 bdb.2

State before:
case h.h
a✝ b✝ : ℝ
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.2943
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3060
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3177
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3294
inst✝¹ : MeasurableSpace α
β : Type ?u.3300
inst✝ : MeasurableSpace β
a b : W → ℝ
ha : Differentiable ℝ a
hb : Differentiable ℝ b
w dw : W
⊢ randFwdDeriv (fun w => uniform (a w) (b w)) w dw =
    let ada := fwdDeriv ℝ a w dw;
    let bdb := fwdDeriv ℝ b w dw;
    fduniform ada.1 bdb.1 ada.2 bdb.2
Tactic:
simp (disch:=sorry) [randFwdDeriv,fwdDeriv,fduniform]
State after:
no goals