Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule_at (SciLean/Core/Functions/Exp.lean)

State before:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ fwdDeriv R (fun w => log (x w)) w = fun dw =>
    let xdx := fwdDeriv R x w dw;
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Tactic:
unfold fwdDeriv
State after:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => ((fun w => log (x w)) w, cderiv R (fun w => log (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)

State before:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => ((fun w => log (x w)) w, cderiv R (fun w => log (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Tactic:
fun_trans (disch:=assumption)
State after:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => (log (x w), (fwdDeriv R (fun w => x w) w dx).2 / abs (fwdDeriv R (fun w => x w) w dx).1)) = fun dw =>
    (log (x w), cderiv R x w dw / abs (x w))

State before:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => (log (x w), (fwdDeriv R (fun w => x w) w dx).2 / abs (fwdDeriv R (fun w => x w) w dx).1)) = fun dw =>
    (log (x w), cderiv R x w dw / abs (x w))
Tactic:
simp[fwdDeriv]
State after:
no goals

State before:
case funProp.discharger
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
dx : W
⊢ x w ≠ 0
Tactic:
assumption
State after:
no goals