-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem changeOrigin_toFormalMultilinearSeries [DecidableEq ι] :
    continuousMultilinearCurryFin1 𝕜 (∀ i, E i) F (f.toFormalMultilinearSeries.changeOrigin x 1) =
    f.linearDeriv x

Proof state:
case h.inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ (∑ a : { s // #s = Fintype.card ι - 1 },
      ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑a ⋯) fun x_1 => x) fun x => y) =
    ∑ i : ι, f (Function.update x i (y i))

Tactic:
simp_rw [changeOriginSeriesTerm_apply]

Result:
case h.inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ∑ x_1 : { s // #s = Fintype.card ι - 1 },
      (f.toFormalMultilinearSeries (1 + (Fintype.card ι - 1))) ((↑x_1).piecewise (fun x_2 => x) fun x => y) =
    ∑ i : ι, f (Function.update x i (y i))

Proof state:
case h.inl
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 => x) (Fin.snoc 0 y) =
    ∑ i : ι, f (Function.update x i (y i))

Tactic:
have (l) : 1 + l ≠ Fintype.card ι := by
  rw [add_comm, Fintype.card_eq_zero]; exact Nat.succ_ne_zero _

Result:
case h.inl
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 => x) (Fin.snoc 0 y) =
    ∑ i : ι, f (Function.update x i (y i))

Proof state:
case right.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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
a : Fin (1 + (Fintype.card ι - 1))
ha : sᶜ = {a}
⊢ ∃ a, (fun x => ⟨{x}ᶜ, ⋯⟩) a = ⟨s, hs⟩

Tactic:
exact ⟨a, Subtype.ext (compl_eq_comm.mp ha)⟩

Result:
no goals

Proof state:
case h.inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ((∑ s : { s // #s = Fintype.card ι - 1 },
          f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯)
        fun x_1 => x)
      (Fin.snoc 0 y) =
    ∑ i : ι, f (Function.update x i (y i))

Tactic:
rw [sum_apply, ContinuousMultilinearMap.sum_apply, Fin.snoc_zero]

Result:
case h.inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ (∑ a : { s // #s = Fintype.card ι - 1 },
      ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑a ⋯) fun x_1 => x) fun x => y) =
    ∑ i : ι, f (Function.update x i (y i))

Proof state:
case right
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
⊢ ∃ a, (fun x => ⟨{x}ᶜ, ⋯⟩) a = ⟨s, hs⟩

Tactic:
have h : #sᶜ = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]

Result:
case right
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
⊢ ∃ a, (fun x => ⟨{x}ᶜ, ⋯⟩) a = ⟨s, hs⟩

Proof state:
case right
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
⊢ ∃ a, (fun x => ⟨{x}ᶜ, ⋯⟩) a = ⟨s, hs⟩

Tactic:
obtain ⟨a, ha⟩ := card_eq_one.mp h

Result:
case right.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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
a : Fin (1 + (Fintype.card ι - 1))
ha : sᶜ = {a}
⊢ ∃ a, (fun x => ⟨{x}ᶜ, ⋯⟩) a = ⟨s, hs⟩

Proof state:
case h.inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
m : ℕ
hm : ¬1 + m = Fintype.card ι
⊢ ((f.toFormalMultilinearSeries.changeOriginSeries 1 m) fun x_1 => x) = 0

Tactic:
rw [f.changeOriginSeries_support hm, zero_apply]

Result:
no goals

Proof state:
case h.inr.refine_3.h.e_6.h.h.inr
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i j : ι
hj : j ≠ i
⊢ Function.update x i (y i) j = if j = i then y j else x j

Tactic:
rw [Function.update_of_ne hj, if_neg hj]

Result:
no goals