-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem derivSeries_apply_diag (n : ℕ) (x : E) :
    derivSeries p n (fun _ ↦ x) x = (n + 1) • p (n + 1) fun _ ↦ x

Proof state:
case h.e'_2.a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x✝ : { s // s.card = n }
a✝ : x✝ ∈ Finset.univ
⊢ ((p.changeOriginSeriesTerm 1 n ↑x✝ ⋯) fun x_1 => x) (Fin.snoc ![] x) = (p (n + 1)) fun x_1 => x

Tactic:
rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ ((p.derivSeries n) fun x_1 => x) x = (n + 1) • (p (n + 1)) fun x_1 => x

Tactic:
simp only [derivSeries, compFormalMultilinearSeries_apply, changeOriginSeries,
  compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
  Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum, coe_sum', Finset.sum_apply,
  continuousMultilinearCurryFin1_apply, Matrix.zero_empty]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ ∑ x_1 : { s // s.card = n }, ((p.changeOriginSeriesTerm 1 n ↑x_1 ⋯) fun x_2 => x) (Fin.snoc ![] x) =
    (n + 1) • (p (n + 1)) fun x_1 => x

Proof state:
case h.e'_3.h.e'_5
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ n + 1 = Finset.univ.card

Tactic:
rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
  Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ ∑ x_1 : { s // s.card = n }, ((p.changeOriginSeriesTerm 1 n ↑x_1 ⋯) fun x_2 => x) (Fin.snoc ![] x) =
    (n + 1) • (p (n + 1)) fun x_1 => x

Tactic:
convert Finset.sum_const _

Result:
case h.e'_2.a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x✝ : { s // s.card = n }
a✝ : x✝ ∈ Finset.univ
⊢ ((p.changeOriginSeriesTerm 1 n ↑x✝ ⋯) fun x_1 => x) (Fin.snoc ![] x) = (p (n + 1)) fun x_1 => x

case h.e'_3.h.e'_5
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ n + 1 = Finset.univ.card