Theorem: Probly.dnormal.density_wrt_normal (Probly/Normal.lean)

State before:
μ σ dμ dσ : ℝ
⊢ DRand.density (dnormal μ σ dμ dσ) ↑(normal μ σ).μ = fun x =>
    (dμ * (x - μ) + dσ * (x - μ - σ) * (x - μ + σ) / σ) / σ ^ 2
Tactic:
sorry
State after:
no goals