Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiff_rule (SciLean/Core/Functions/Pow.lean)

State before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
⊢ HasAdjDiff R fun u => sqrt (x u)
Tactic:
intro u
State after:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ HasAdjDiffAt R (fun u => sqrt (x u)) u

State before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ HasAdjDiffAt R (fun u => sqrt (x u)) u
Tactic:
fun_prop (disch:=aesop)
State after:
no goals

State before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ 0 < x u
Tactic:
aesop
State after:
no goals