awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n f =
    Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
have h : ∀ (x : 𝕜),
  iteratedDeriv n f x =
    Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDeriv n f)
have rw : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
  (Function.comp (β := F)
    (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
      (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
Tactic: rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    (Function.comp (β := F)
      (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDeriv n f)
have rw₁ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
  (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (Function.comp (β := F)
        (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        (⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
      ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
Tactic: rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    (Function.comp (β := F)
      (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
rw₁ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := F)
          (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
          (⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDeriv n f)
have rw₂ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f) (id ∘ iteratedFDeriv 𝕜 n f)
Tactic: rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    (Function.comp (β := F)
      (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
rw₁ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (Function.comp (β := F)
          (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
          (⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
rw₂ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f) (id ∘ iteratedFDeriv 𝕜 n f)
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDeriv n f)
have rw₃ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f) (iteratedFDeriv 𝕜 n f)
Tactic: rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) m =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ i : Fin n, m i) (iteratedDeriv n f x)
have rw : Eq.{u_2 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) m : F)
  ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (i : Fin n) ↦ HSMul.hSMul (β := 𝕜) (m i) 1 : F)
Tactic: rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) = ‖iteratedDeriv n f x‖
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) =
  norm.{u_2} (E := F)
    (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
      (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
Tactic: rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) =
    norm.{u_2} (E := F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) = ‖iteratedDeriv n f x‖
have rw₁ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) =
  norm.{u_2} (E := F)
    ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDeriv 𝕜 n f x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
      F)
Tactic: rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) =
    norm.{u_2} (E := F)
      (Function.comp (β := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
        ((⇑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
        (iteratedFDeriv 𝕜 n f : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) =
    norm.{u_2} (E := F)
      ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
          (iteratedFDeriv 𝕜 n f x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
        F)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) = ‖iteratedDeriv n f x‖
have rw₂ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) =
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
    (iteratedFDeriv 𝕜 n f x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
Tactic: rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ iteratedDeriv 0 f = f
have h : ∀ (x : 𝕜), iteratedDeriv 0 f x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ iteratedDeriv 1 f = deriv f
have h : ∀ (x : 𝕜), iteratedDeriv 1 f x = deriv f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔
    (∀ m ≤ n,
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv m f)) ∧
      ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)
have rw : ((∀ (m : ℕ),
      LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) →
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv m f)) ∧
    ∀ (m : ℕ), LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → Differentiable 𝕜 (iteratedDeriv m f)) ↔
  (∀ m ≤ n,
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (iteratedDeriv m f)) ∧
    ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)
Tactic: rw [← WithTop.coe_natCast, contDiff_iff_iteratedDeriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)
have rw : iteratedDerivWithin (n + 1) f univ = derivWithin (iteratedDerivWithin n f univ) univ
Tactic: rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n f = deriv^[n] f
have h : ∀ (x : 𝕜), iteratedDeriv n f x = deriv^[n] f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv n f x = deriv^[n] f x
have h : iteratedDerivWithin n f univ x = deriv^[n] f x
Tactic: rw [← iteratedDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = deriv^[n] f x
have h : ∀ (x : 𝕜 → F), deriv x = derivWithin x univ
Tactic: convert! iteratedDerivWithin_eq_iterate (F := F)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
have simp_rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
Tactic: simp_rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_of_isOpen n hs hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
simp_rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
have simp_rw₁ : Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
  ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: simp_rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_of_isOpen n hs hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
s t : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
r : 𝕜
hr : r ∈ s ∩ t
⊢ iteratedDerivWithin n f s r = iteratedDerivWithin n f t r
have rw : iteratedDeriv n f r = iteratedDerivWithin n f t r
Tactic: rw [iteratedDerivWithin_of_isOpen hs hr.1, iteratedDerivWithin_of_isOpen ht hr.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
s t : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
r : 𝕜
hr : r ∈ s ∩ t
rw : iteratedDeriv n f r = iteratedDerivWithin n f t r
⊢ iteratedDerivWithin n f s r = iteratedDerivWithin n f t r
have rw₁ : iteratedDeriv n f r = iteratedDeriv n f r
Tactic: rw [iteratedDerivWithin_of_isOpen hs hr.1, iteratedDerivWithin_of_isOpen ht hr.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (iteratedDerivWithin n f s) (deriv^[n] f) s
have apply : EqOn (iteratedDeriv n f) (deriv^[n] f) s
Tactic: apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (iteratedDeriv n f) (deriv^[n] f) s
have rw : EqOn (deriv^[n] f) (deriv^[n] f) s
Tactic: rw [iteratedDeriv_eq_iterate]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
have rw : deriv^[n + 1] f = iteratedDeriv n (deriv f)
Tactic: rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate, Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw : deriv^[n + 1] f = iteratedDeriv n (deriv f)
⊢ iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
have rw₁ : deriv^[n + 1] f = deriv^[n] (deriv f)
Tactic: rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate, Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw : deriv^[n + 1] f = iteratedDeriv n (deriv f)
rw₁ : deriv^[n + 1] f = deriv^[n] (deriv f)
⊢ iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
have rw₂ : deriv^[n] (deriv f) = deriv^[n] (deriv f)
Tactic: rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate, Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
h : AnalyticAt 𝕜 f x
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
have obtain : ∀ (p : FormalMultilinearSeries 𝕜 𝕜 𝕜) (hp : HasFPowerSeriesAt f p x),
  HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
have h : (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p
Tactic: convert! hp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p
have h : ∀ (r : ENNReal) (hpr : HasFPowerSeriesOnBall f p x r),
  (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p
Tactic: obtain ⟨r, hpr⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p
have h : ∀ (n : ℕ),
  Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) n :
          (a : (i : Fin n) → 𝕜) → 𝕜)
        fun (x : Fin n) ↦ 1 :
      𝕜)
    ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (hypothesis)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
⊢ Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) n :
          (a : (i : Fin n) → 𝕜) → 𝕜)
        fun (x : Fin n) ↦ 1 :
      𝕜)
    ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜)
have h_fact_smul : ∀ (n : ℕ),
  HSMul.hSMul (β := 𝕜) n.factorial ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜) =
    (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
Tactic: have h_fact_smul := hpr.factorial_smul 1