-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_succ_apply_right {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s)
    (m : Fin (n + 1) → E) :
    (iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m =
      iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x (init m) (m (last n))

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 : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))

Tactic:
induction' n with n IH generalizing x

Result:
case zero
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin (0 + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (0 + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 0 (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last 0))

case succ
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last (n + 1)))

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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun i => E) (E →L[𝕜] F) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F :=
  (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
y : E
hy : y ∈ s
⊢ iteratedFDerivWithin 𝕜 n.succ f s y = (⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y

Tactic:
ext m

Result:
case 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m✝ : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun i => E) (E →L[𝕜] F) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F :=
  (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
y : E
hy : y ∈ s
m : Fin n.succ → E
⊢ (iteratedFDerivWithin 𝕜 n.succ f s y) m = ((⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y) m

Proof state:
case succ
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last (n + 1)))

Tactic:
let I := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm

Result:
case succ
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun i => E) (E →L[𝕜] F) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F :=
  (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
⊢ (iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last (n + 1)))

Proof state:
case 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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m✝ : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun i => E) (E →L[𝕜] F) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F :=
  (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
y : E
hy : y ∈ s
m : Fin n.succ → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s y) (init m)) (m (last n)) =
    ((⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y) m

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
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E},
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun i => E) (E →L[𝕜] F) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F :=
  (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y = (⇑I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (⇑I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x) (m 0)) (tail m)

Tactic:
rw [fderivWithin_congr A (A x hx)]

Result:
no goals