fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
R✝ : Type ?u.29295
C : Type ?u.29294
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.29304
inst✝⁴ : Vec C W✝
U✝ : Type ?u.29327
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.29349
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), x u ≠ 0
⊢ (fun x_1 => ((fun u => log (x u)) x_1, semiAdjoint R (cderiv R (fun u => log (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
no goals