simp
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + 0 = ((innerSL ℝ) u) dx
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (ContinuousLinearMap.id ℝ E)) u) dx = ((innerSL ℝ) u) dx