no goals
𝕜 : Type u_2
inst✝¹⁶ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁵ : NormedAddCommGroup D
inst✝¹⁴ : NormedSpace 𝕜 D
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type uF
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
G : Type uG
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
X : Type ?u.3124593
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
p' : E → FormalMultilinearSeries 𝕜' E F
h : HasFTaylorSeriesUpToOn n f p' s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => FormalMultilinearSeries.restrictScalars 𝕜 (p' x) m)
    (ContinuousMultilinearMap.curryLeft (FormalMultilinearSeries.restrictScalars 𝕜 (p' x) (Nat.succ m))) s x
simpa only using (ContinuousMultilinearMap.restrictScalarsLinear 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x <|
    (h.fderivWithin m hm x hx).restrictScalars 𝕜