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

State before:
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ CDifferentiable R fun w => log (x w)
Tactic:
intro x
State after:
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => log (x✝ w)) x

State before:
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => log (x✝ w)) x
Tactic:
fun_prop (disch:=aesop)
State after:
no goals

State before:
case funProp.discharger
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ x✝ x ≠ 0
Tactic:
aesop
State after:
no goals