-- 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:
𝕜 : 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)
⊢ HasFDerivWithinAt (⇑(continuousMultilinearCurryFin0 𝕜 E F) ∘ fun x => p x 0)
    ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x

Tactic:
rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']

Result:
𝕜 : 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)
⊢ 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

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 i = cons y v i

Tactic:
rw [Unique.eq_default (α := Fin 1) i]

Result:
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

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)
⊢ 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:
have : ((0 : ℕ) : ℕ∞) < n := zero_lt_one.trans_le hn

Result:
𝕜 : 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

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
⊢ (p x 1) (snoc 0 y) = (p x 1) (cons y v)

Tactic:
congr with i

Result:
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 i = cons y v i

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
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x

Tactic:
have A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0) := fun y hy ↦
  (h.zero_eq y hy).symm

Result:
𝕜 : 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)
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x