no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.77069
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.77198
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
x : ℝ
⊢ HasDerivAt f f' x →
    HasDerivAt g g' x → HasDerivAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) x
simpa only [← hasDerivWithinAt_univ] using HasDerivWithinAt.inner 𝕜