Theorem: SciLean.gaussian.arg_μx.cderiv_rule (SciLean/Core/Functions/Gaussian.lean)

State before:
R : Type u_1
C : Type ?u.17858
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
⊢ (fwdDeriv R fun w => gaussian (μ w) σ (x w)) = fun w dw =>
    let μdμ := fwdDeriv R μ w dw;
    let xdx := fwdDeriv R x w dw;
    let xdx' := σ⁻¹ • (xdx - μdμ);
    let g := gaussian μdμ.1 σ xdx.1;
    (g, -⟪xdx'.1, xdx'.2⟫_R * g)
Tactic:
sorry_proof
State after:
no goals