awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F) (f.iteratedFDeriv (E₁ := E) n x) ≤
    (↑((Fintype.card ι).descFactorial n) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

Tactic:
f.norm_iteratedFDeriv_le' n x

Premises used: ContinuousMultilinearMap.norm_iteratedFDeriv_le'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F) (f.iteratedFDeriv (E₁ := E) n x) ≤
    (↑((Fintype.card ι).descFactorial n) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

Tactic:
exact f.norm_iteratedFDeriv_le' n x

Premises used: ContinuousMultilinearMap.norm_iteratedFDeriv_le'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
simp :
  ∑ x_1 : { s : Finset (Fin (1 + n)) // s.card = n },
      ((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) =
    HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)
⊢ ((p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x_1 : Fin n) ↦ x : (a : E) → F) x =
    HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)

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]

Premises used: FormalMultilinearSeries.derivSeries, Finset.sum_apply, FormalMultilinearSeries.changeOriginSeries, ContinuousMultilinearMap.sum_apply, ContinuousLinearMap.compFormalMultilinearSeries_apply, LinearIsometryEquiv.coe_coe, map_sum, ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearMap.coe_sum', Function.comp_apply, ContinuousLinearEquiv.coe_coe, Matrix.zero_empty, continuousMultilinearCurryFin1_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ (∑ _x : { s : Finset (Fin (1 + n)) // s.card = n },
      (p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (β := F) (Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ)
      ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)

Tactic:
Finset.sum_const _

Premises used: Finset.sum_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h :
  ∀ (x_1 : { s : Finset (Fin (1 + n)) // s.card = n }),
    Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1 →
      Eq.{v + 1} (α := F)
        (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
                  (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
                fun (x_2 : Fin n) ↦ x :
              (a : (i : Fin 1) → E) → F)
            (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
          F)
        ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₁ : n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
⊢ ∑ x_1 : { s : Finset (Fin (1 + n)) // s.card = n },
      ((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) =
    HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)

Tactic:
convert! Finset.sum_const _

Premises used: Finset.sum_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x_1 : { s : Finset (Fin (1 + n)) // s.card = n }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1
h :
  Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        fun (x_2 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₁ :
  Eq.{v + 1} (α := F)
    ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F)
        ((↑x_1 : Finset (Fin (1 + n))).piecewise (π := fun (i : Fin (1 + n)) ↦ E) (fun (x_2 : Fin (1 + n)) ↦ x)
          fun (x_2 : Fin (1 + n)) ↦ x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₂ :
  Eq.{v + 1} (α := F) ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F) fun (x_2 : Fin (1 + n)) ↦ x : F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₃ h₄ :
  Eq.{v + 1} (α := F) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
⊢ Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)

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

Premises used: FormalMultilinearSeries.changeOriginSeriesTerm_apply, add_comm, Fin.snoc_zero, Finset.piecewise_same
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
h₅ : n + 1 = (card (Fin (1 + n))).choose n
h₆ : n + 1 = (1 + n).choose n
h₇ : (1 + n).choose n = n + 1
h₈ : (n + 1).choose n = n + 1
h₉ h₁₀ : n + 1 = n + 1
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ

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]

Premises used: Fintype.card_fin, Nat.choose_succ_self_right, Fintype.card, Finset.powersetCard_eq_filter, eq_comm, Fintype.card_subtype, add_comm, Finset.card_powersetCard, Finset.powerset_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 𝕜 F
n : ℕ
⊢ (coeff (𝕜 := 𝕜) p.derivSeries n : (a : 𝕜) → F) 1 = (n + 1) • p.coeff (n + 1)

Tactic:
p.derivSeries_apply_diag _ _

Premises used: Multiset.powerset, FormalMultilinearSeries.coeff, Multiset.ofList, FormalMultilinearSeries.derivSeries_apply_diag, Multiset.filter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
H :
  ∀ (x_1 : (i : Fin 0) → E),
    Eq.{v + 1} (α := F) ((iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) x_1 : F)
      ((p 0 : (a : (i : Fin 0) → E) → F) x_1 : F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f x) (p 0)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x_1 : (i : Fin 0) → E
⊢ Eq.{v + 1} (α := F) ((iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) x_1 : F)
    ((p 0 : (a : (i : Fin 0) → E) → F) x_1 : F)

Tactic:
simpa using (coeff_zero h _).symm

Premises used: HasFPowerSeriesOnBall.coeff_zero, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
⊢ ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
zero :
  ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
        {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
        HasFPowerSeriesOnBall f p x r →
          HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
            (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y
⊢ ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y

Tactic:
induction n with | zero => _ | succ n ih => _

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
zero :
  ∀ [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F}
    {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
⊢ ∀ [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F}
    {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst_3 : NormedAddCommGroup F
zero :
  ∀ [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
⊢ ∀ [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
zero :
  ∀ [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
⊢ ∀ [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
        (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
F : Type (max u v)
succ :
  ∀ [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F}
    {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y
⊢ ∀ [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F}
    {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
F : Type (max u v)
inst_3 : NormedAddCommGroup F
succ :
  ∀ [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y
⊢ ∀ [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
F : Type (max u v)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
succ :
  ∀ [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y
⊢ ∀ [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
        (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
zero :
  HSMul.hSMul (α := ℕ) (β := F) 1 ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
    (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
zero₁ :
  Eq (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
    ((iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
zero₂ zero₃ :
  Eq (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
    ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
⊢ HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
    (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y

Tactic:
rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]

Premises used: one_smul, HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag, Nat.factorial_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
F : Type (max u v)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
succ :
  Eq (α := F)
    (((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y : (a : E) → F) y : F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
⊢ HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
    (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y

Tactic:
rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← ContinuousLinearMap.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]

Premises used: ContinuousLinearMap.smul_apply, Nat.factorial_succ, HasFPowerSeriesOnBall.fderiv, iteratedFDeriv_succ_apply_right, mul_comm, FormalMultilinearSeries.derivSeries_apply_diag, SemigroupAction.mul_smul