-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpToOn.hasFDerivWithinAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n)
    (hx : x ∈ s) : HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x

Proof state:
case h.e'_12.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
he✝ : NormedSpace.toModule = ContinuousMultilinearMap.instModule
e_10✝ : UniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
⊢ (↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }).comp
      ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) =
    (p x (Nat.succ 0)).curryLeft

Tactic:
ext y v

Result:
case h.e'_12.h.h.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
he✝ : NormedSpace.toModule = ContinuousMultilinearMap.instModule
e_10✝ : UniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
y : E
v : Fin 0 → E
⊢ (((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)))
        y)
      v =
    ((p x (Nat.succ 0)).curryLeft y) v

Proof state:
case h.e'_12.h.h.h.H.h.e_6.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
he✝ : NormedSpace.toModule = ContinuousMultilinearMap.instModule
e_10✝ : UniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
y : E
v : Fin 0 → E
i : Fin (0 + 1)
⊢ snoc 0 y default = cons y v default

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
⊢ HasFDerivWithinAt (fun x => p x 0)
    ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }).comp
      ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)))
    s x

Tactic:
convert h.fderivWithin _ this x hx

Result:
case h.e'_12.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
he✝ : NormedSpace.toModule = ContinuousMultilinearMap.instModule
e_10✝ : UniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
⊢ (↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }).comp
      ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) =
    (p x (Nat.succ 0)).curryLeft

Proof state:
case h.e'_12.h.h.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
he✝ : NormedSpace.toModule = ContinuousMultilinearMap.instModule
e_10✝ : UniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
y : E
v : Fin 0 → E
⊢ (((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)))
        y)
      v =
    ((p x (Nat.succ 0)).curryLeft y) v

Tactic:
change (p x 1) (snoc 0 y) = (p x 1) (cons y v)

Result:
case h.e'_12.h.h.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : 1 ≤ n
hx : x ∈ s
A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)
this : ↑↑0 < n
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = ContinuousMultilinearMap.instAddCommGroup
he✝ : NormedSpace.toModule = ContinuousMultilinearMap.instModule
e_10✝ : UniformSpace.toTopologicalSpace = ContinuousMultilinearMap.instTopologicalSpace
y : E
v : Fin 0 → E
⊢ (p x 1) (snoc 0 y) = (p x 1) (cons y v)