-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt (hn : n ≠ ∞) :
    ContDiffWithinAt 𝕜 (n + 1) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, (n = ω → AnalyticOn 𝕜 f u) ∧
      ∃ f' : E → E →L[𝕜] F,
      (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
𝕜 : 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 ℕ∞
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p' x i) v
⊢ n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => (fun x => (p' x).unshift (f x)) x i) (v ∩ u)

Tactic:
intro h i

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
𝕜 : 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 ℕ∞
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p' x i) v
h : n + 1 = ω
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (fun x => (p' x).unshift (f x)) x i) (v ∩ u)

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 ℕ∞
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p' x i) v
i✝ : ℕ
h : n = ω
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (fun x => (p' x).unshift (f x)) x (i + 1)) (v ∩ u)

Tactic:
simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one]

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 ℕ∞
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p' x i) v
i✝ : ℕ
h : n = ω
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (continuousMultilinearCurryRightEquiv' 𝕜 i E F).symm (p' x i)) (v ∩ u)

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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : ω ≠ ∞
h'n : ω + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (ω + 1) f s x
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn ω (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) u
H'p : ω + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => p x (i + 1)) u

Tactic:
exact H'p rfl _

Result:
no goals

Proof state:
case h.e'_12.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 ℕ∞
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p' x i) v
y : E
hy : y ∈ v ∩ u
z : E
⊢ ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        ((p' y).unshift (f y) 1).curryLeft)
      z =
    (p' y 0).curry0 z

Tactic:
change ((p' y 0) (init (@cons 0 (fun _ => E) z 0))) (@cons 0 (fun _ => E) z 0 (last 0)) =
  ((p' y 0) 0) z

Result:
case h.e'_12.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 ℕ∞
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p' x i) v
y : E
hy : y ∈ v ∩ u
z : E
⊢ ((p' y 0) (init (cons z 0))) (cons z 0 (last 0)) = ((p' y 0) 0) z

Proof state:
case mp.intro.intro.intro.intro.refine_2.refine_2
𝕜 : 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : ω ≠ ∞
h'n : ω + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (ω + 1) f s x
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn ω (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) u
H'p : ω + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (fun y => (p y).shift) x i) u

Tactic:
change AnalyticOn 𝕜
  (fun x ↦ (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u

Result:
case mp.intro.intro.intro.intro.refine_2.refine_2
𝕜 : 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : ω ≠ ∞
h'n : ω + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (ω + 1) f s x
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn ω (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) u
H'p : ω + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u