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

Proof state:
case fderiv
𝕜 : 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
⊢ HasFDerivAt (fun y => f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x

Tactic:
suffices H : curryLeft (f.iteratedFDeriv (Nat.succ n) x) = (∑ e : Fin n ↪ ι,
      ((iteratedFDerivComponent f e.toEquivRange).linearDeriv
        (Pi.compRightL 𝕜 _ Subtype.val x)) ∘L (Pi.compRightL 𝕜 _ Subtype.val)) by
  have A : HasFDerivAt (f.iteratedFDeriv n) (∑ e : Fin n ↪ ι,
      ((iteratedFDerivComponent f e.toEquivRange).linearDeriv (Pi.compRightL 𝕜 _ Subtype.val x))
        ∘L (Pi.compRightL 𝕜 _ Subtype.val)) x := by
    apply HasFDerivAt.sum (fun s _hs ↦ ?_)
    exact (ContinuousMultilinearMap.hasFDerivAt _ _).comp x (ContinuousLinearMap.hasFDerivAt _)
  rwa [← H] at A

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

Proof state:
case intro
𝕜 : 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 ↪ ι
j : Fin n.succ
hkf : e j ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ e j = e 0

Tactic:
simpa using hkf

Result:
no goals

Proof state:
case neg.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
e : Fin n.succ ↪ ι
k : ι
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hke : ⟨k, ⋯⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ e 0 ∈ range ⇑e

Tactic:
exact Set.mem_range_self _

Result:
no goals

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
⊢ ((f.iteratedFDeriv n.succ x).curryLeft v) m =
    ((∑ e : Fin n ↪ ι,
          ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
            (Pi.compRightL 𝕜 E Subtype.val))
        v)
      m

Tactic:
simp only [ContinuousMultilinearMap.iteratedFDeriv, curryLeft_apply, sum_apply,
  iteratedFDerivComponent_apply, Finset.univ_sigma_univ,
  Pi.compRightL_apply, ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
  Finset.sum_apply, Function.comp_apply, linearDeriv_apply, Finset.sum_sigma']

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) =
    ∑ 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⟩

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) =
    ∑ 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⟩

Tactic:
congr with e

Result:
case fderiv.h.H.e_f.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
e : Fin n.succ ↪ ι
⊢ (f fun j => if h : j ∈ range ⇑e then Fin.cons v m (e.toEquivRange.symm ⟨j, ⋯⟩) j else x j) =
    f fun j =>
      if h : j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst then
        m (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨j, h⟩) j
      else
        Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) e).snd
          (v ↑((Equiv.embeddingFinSucc n ι) e).snd) ⟨j, h⟩

Proof state:
case neg.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
e : Fin n.succ ↪ ι
k : ι
hke : k ∉ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ ⟨k, ⋯⟩ ≠ ((Equiv.embeddingFinSucc n ι) e).snd

Tactic:
contrapose! hke

Result:
case neg.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
e : Fin n.succ ↪ ι
k : ι
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hke : ⟨k, ⋯⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ k ∈ range ⇑e

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)
A :
  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
⊢ HasFDerivAt (fun y => f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x

Tactic:
rwa [← H] at A

Result:
no goals