-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem hasFTaylorSeriesUpTo_iteratedFDeriv :
    HasFTaylorSeriesUpTo ⊤ f (fun v n ↦ f.iteratedFDeriv n v)

Proof state:
case neg
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
hke : e 0 ∈ range ⇑e
hkf : e 0 ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ v (e 0) =
    if h : ⟨e 0, hkf⟩ = ((Equiv.embeddingFinSucc n ι) e).snd then v ↑((Equiv.embeddingFinSucc n ι) e).snd else x (e 0)

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
hke : e 0 ∈ range ⇑e
hkf : e 0 ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
h : ⟨e 0, hkf⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ v (e 0) = v ↑((Equiv.embeddingFinSucc n ι) e).snd

case neg
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
hke : e 0 ∈ range ⇑e
hkf : e 0 ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
h : ¬⟨e 0, hkf⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ v (e 0) = x (e 0)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
e : Fin n ↪ ι
x✝ : e ∈ Finset.univ
⊢ Continuous fun a => (f.iteratedFDerivComponent e.toEquivRange) ((Pi.compRightL 𝕜 E Subtype.val) a)

Tactic:
exact (ContinuousMultilinearMap.coe_continuous _).comp (ContinuousLinearMap.continuous _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e : Fin n ↪ ι,
      ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
        (Pi.compRightL 𝕜 E Subtype.val)
⊢ HasFDerivAt (f.iteratedFDeriv n)
    (∑ e : Fin n ↪ ι,
      ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
        (Pi.compRightL 𝕜 E Subtype.val))
    x

Tactic:
apply HasFDerivAt.sum (fun s _hs ↦ ?_)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e : Fin n ↪ ι,
      ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
        (Pi.compRightL 𝕜 E Subtype.val)
s : Fin n ↪ ι
_hs : s ∈ Finset.univ
⊢ HasFDerivAt (fun y => (f.iteratedFDerivComponent s.toEquivRange) ((Pi.compRightL 𝕜 E Subtype.val) y))
    (((f.iteratedFDerivComponent s.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
      (Pi.compRightL 𝕜 E Subtype.val))
    x

Proof state:
case fderiv.h.H
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
⊢ (∑ x_1 : Fin n.succ ↪ ι,
      f fun j => if h : j ∈ range ⇑x_1 then Fin.cons v m (x_1.toEquivRange.symm ⟨j, ⋯⟩) j else x j) =
    ∑ x_1 : (i : Fin n ↪ ι) × { a // a ∉ range ⇑i },
      f fun j =>
        if h : j ∈ range ⇑x_1.fst then m (x_1.fst.toEquivRange.symm ⟨j, h⟩) j
        else Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) x_1.snd (v ↑x_1.snd) ⟨j, h⟩

Tactic:
rw [← (Equiv.embeddingFinSucc n ι).sum_comp]

Result:
case fderiv.h.H
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
⊢ (∑ x_1 : Fin n.succ ↪ ι,
      f fun j => if h : j ∈ range ⇑x_1 then Fin.cons v m (x_1.toEquivRange.symm ⟨j, ⋯⟩) j else x j) =
    ∑ i : Fin (n + 1) ↪ ι,
      f fun j =>
        if h : j ∈ range ⇑((Equiv.embeddingFinSucc n ι) i).fst then
          m (((Equiv.embeddingFinSucc n ι) i).fst.toEquivRange.symm ⟨j, h⟩) j
        else
          Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) i).snd
            (v ↑((Equiv.embeddingFinSucc n ι) i).snd) ⟨j, h⟩

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ k ∈ range ⇑e

Tactic:
rw [Equiv.embeddingFinSucc_fst] at hke

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∈ range (⇑e ∘ Fin.succ)
⊢ k ∈ range ⇑e