-- 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 ↪ ι
k : ι
hke : k ∈ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ Fin.cons v m (e.toEquivRange.symm ⟨k, ⋯⟩) k =
    Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) e).snd
      (v ↑((Equiv.embeddingFinSucc n ι) e).snd) ⟨k, hkf⟩

Tactic:
obtain rfl : k = e 0 := by
  rcases hke with ⟨j, rfl⟩
  simpa using hkf

Result:
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
⊢ Fin.cons v m (e.toEquivRange.symm ⟨e 0, ⋯⟩) (e 0) =
    Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) e).snd
      (v ↑((Equiv.embeddingFinSucc n ι) e).snd) ⟨e 0, hkf⟩

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 ↪ ι
k : ι
hke : k ∉ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ x k =
    Function.update (fun i => x ↑i) ((Equiv.embeddingFinSucc n ι) e).snd (v ↑((Equiv.embeddingFinSucc n ι) e).snd)
      ⟨k, ⋯⟩

Tactic:
rw [Function.update_of_ne]

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

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 (⇑e ∘ Fin.succ)
⊢ k ∈ range ⇑e

Tactic:
exact Set.range_comp_subset_range _ _ hke

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 v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∉ range ⇑e
⊢ k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst

Tactic:
contrapose! 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 ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ k ∈ range ⇑e

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
⊢ ∀ (m : ℕ),
    ↑m < ⊤ → ∀ (x : (i : ι) → E i), HasFDerivAt (fun y => f.iteratedFDeriv m y) (f.iteratedFDeriv m.succ x).curryLeft x

Tactic:
rintro n - x

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

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 ↪ ι
k : ι
hke : k ∉ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ (if h : k ∈ range ⇑e then Fin.cons v m (e.toEquivRange.symm ⟨k, ⋯⟩) k else x k) =
    if h : k ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst then
      m (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨k, h⟩) k
    else
      Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) e).snd
        (v ↑((Equiv.embeddingFinSucc n ι) e).snd) ⟨k, h⟩

Tactic:
simp only [hke, hkf, ↓reduceDIte, Pi.compRightL,
  ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk]

Result:
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 ↪ ι
k : ι
hke : k ∉ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ x k =
    Function.update (fun i => x ↑i) ((Equiv.embeddingFinSucc n ι) e).snd (v ↑((Equiv.embeddingFinSucc n ι) e).snd)
      ⟨k, ⋯⟩

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 ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ k = e 0

Tactic:
rcases hke with ⟨j, rfl⟩

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