Theorem: SciLean.Scalar.exp.arg_x.HasAdjDiff_rule (SciLean/Core/Functions/Exp.lean)

State before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ HasAdjDiff C fun u => exp (x u)
Tactic:
intro x
State after:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => exp (x✝ u)) x

State before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => exp (x✝ u)) x
Tactic:
constructor
State after:
case left
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => exp (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)

State before:
case left
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => exp (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)
Tactic:
fun_prop
State after:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)

State before:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)
Tactic:
fun_trans [fwdDeriv]
State after:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * exp (x✝ x)

State before:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * exp (x✝ x)
Tactic:
fun_prop
State after:
no goals