awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f x) (p 0)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
⊢ ∀ {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
have 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
Tactic: induction n with | zero => _ | succ n ih => _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ ∀ {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
have 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
Tactic: induction n with | zero => _ | succ n ih => _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ 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
have 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
Tactic: rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ 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
have 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)
Tactic: rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
⊢ 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
have 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)
Tactic: rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ 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
have 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)
Tactic: rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← ContinuousLinearMap.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
y : E
inst_5 : CompleteSpace F
n : ℕ
⊢ 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
have zero : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
y : E
inst_5 : CompleteSpace F
n : ℕ
zero :
  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
⊢ 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
have succ : ∀ (n : ℕ),
  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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
y : E
inst_5 : CompleteSpace 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
have 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
Tactic: rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
y : E
inst_5 : CompleteSpace F
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
⊢ 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
have zero₁ : Eq.{v + 1} (α := 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)
Tactic: rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
y : E
inst_5 : CompleteSpace F
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.{v + 1} (α := 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)
⊢ 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
have zero₂ : Eq.{v + 1} (α := 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)
Tactic: rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
y : E
inst_5 : CompleteSpace F
n : ℕ
⊢ 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
have succ : Eq.{v + 1} (α := 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)
Tactic: rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← ContinuousLinearMap.smul_apply, factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F))
    (f (x + y))
have h₁ : ∀ (n : ℕ),
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
Tactic: convert! h.hasSum hy with n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
have h₁ : HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
    (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
  (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
Tactic: rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
h₁ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
      (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
have h₂ : n ! •
    HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹ ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
  (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
Tactic: rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
h₁ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
      (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₂ :
  n ! •
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
have h₃ : HSMul.hSMul (β := F) (HSMul.hSMul (β := 𝕜) n ! (↑n ! : 𝕜)⁻¹)
    ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
  (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
Tactic: rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
h₁ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
      (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₂ :
  n ! •
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₃ :
  HSMul.hSMul (β := F) (HSMul.hSMul (β := 𝕜) n ! (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
have h₄ : HSMul.hSMul (β := F) (HMul.hMul (α := 𝕜) (↑n ! : 𝕜) (↑n ! : 𝕜)⁻¹)
    ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
  (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
Tactic: rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
h₁ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
      (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₂ :
  n ! •
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₃ :
  HSMul.hSMul (β := F) (HSMul.hSMul (β := 𝕜) n ! (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₄ :
  HSMul.hSMul (β := F) (HMul.hMul (α := 𝕜) (↑n ! : 𝕜) (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
have h₅ : HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) 1 ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
  (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
Tactic: rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
h₁ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
      (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₂ :
  n ! •
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₃ :
  HSMul.hSMul (β := F) (HSMul.hSMul (β := 𝕜) n ! (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₄ :
  HSMul.hSMul (β := F) (HMul.hMul (α := 𝕜) (↑n ! : 𝕜) (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₅ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) 1 ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
have h₆ : Eq.{v + 1} (α := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)
  ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)
Tactic: rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
have rw : Tendsto (fun (n : α) ↦ x + d n) l (𝓝 x) ∧ ∀ᶠ (n : α) in l, x + d n ∈ s
Tactic: rw [tendsto_nhdsWithin_iff]