field_simp [mul_comm]
case h.e_y
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
dy : R
⊢ (sqrt (x u))⁻¹ * 2⁻¹ * dy = dy / (2 * sqrt (x u))
no goals