no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53238
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.53367
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f✝ g✝ : G → E
f'✝ g'✝ : G →L[ℝ] E
s✝ : Set G
x✝ : G
n : ℕ∞
f g : ℝ → E
f' g' : E
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
⊢ HasDerivWithinAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) s x
simpa using (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).hasDerivWithinAt