unfold gaussian
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ log (gaussian μ σ x) =
    let x' := σ⁻¹ • (x - μ);
    -‖x'‖₂² / 2 - log σ - log (sqrt (2 * pi))
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ log
      (let x' := σ⁻¹ • (x - μ);
      1 / (σ * sqrt (2 * pi)) * exp (-‖x'‖₂² / 2)) =
    let x' := σ⁻¹ • (x - μ);
    -‖x'‖₂² / 2 - log σ - log (sqrt (2 * pi))