awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
pos :
  Eq.{u_2 + 1} (α := F)
    (((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n)
              (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1) :
            ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
⊢ Eq.{u_2 + 1} (α := F)
    ((((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                  (↑(↑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
                        F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
                    F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
                  (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) :
                𝕜 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
              (a : 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
            1 :
          (a : (i : Fin n) → 𝕜) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ 𝕜) fun (x : Fin (n + 1)) ↦ 1 : (i : Fin n) → 𝕜) :
      F)
    (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)

Tactic:
change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
      (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
      (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1

Premises used: iteratedDerivWithin, fderivWithin, ContinuousMultilinearMap.mkPiRing, OfNat.ofNat, Fin, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ Eq.{u_2 + 1} (α := F)
    (((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n)
              (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1) :
            ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    (((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : ¬AccPt x (𝓟 s)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
simp [derivWithin_zero_of_not_accPt hxs, iteratedDerivWithin, iteratedFDerivWithin,
      fderivWithin_zero_of_not_accPt hxs]

Premises used: fderivWithin_zero_of_not_accPt, iteratedDerivWithin, iteratedFDerivWithin, derivWithin_zero_of_not_accPt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 0 f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[0] f x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x
x : 𝕜
succ :
  derivWithin (iteratedDerivWithin n f s) s x =
    ((fun (g : 𝕜 → F) ↦ derivWithin g s) ∘ (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n]) f x
⊢ iteratedDerivWithin (n + 1) f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x

Tactic:
rw [iteratedDerivWithin_succ, Function.iterate_succ']

Premises used: Function.iterate_succ', iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n f s) s x =
    ((fun (g : 𝕜 → F) ↦ derivWithin g s) ∘ (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n]) f x

Tactic:
derivWithin_congr (fun y hy => IH) IH

Premises used: derivWithin_congr, derivWithin
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n f s) s x =
    ((fun (g : 𝕜 → F) ↦ derivWithin g s) ∘ (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n]) f x

Tactic:
exact derivWithin_congr (fun y hy => IH) IH

Premises used: derivWithin_congr
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
zero : ∀ {x : 𝕜}, iteratedDerivWithin 0 f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[0] f x
succ :
  ∀ (n : ℕ) (IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x) {x : 𝕜},
    iteratedDerivWithin (n + 1) f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x
⊢ iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] f x

Tactic:
induction n generalizing x with
  | zero => simp
  | succ n IH =>
    rw [iteratedDerivWithin_succ, Function.iterate_succ']
    exact derivWithin_congr (fun y hy => IH) IH

Premises used: Function.iterate_succ', iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
h : ∀ (x : 𝕜), iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x
⊢ iteratedDerivWithin (n + 1) f s = iteratedDerivWithin n (derivWithin f s) s

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
h : (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] (derivWithin f s) x
⊢ iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x

Tactic:
rw [iteratedDerivWithin_eq_iterate, iteratedDerivWithin_eq_iterate]

Premises used: iteratedDerivWithin_eq_iterate
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n + 1] f x = (fun (g : 𝕜 → F) ↦ derivWithin g s)^[n] (derivWithin f s) x

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
simp :
  ((∀ m ≤ n + 1, ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ m < n + 1, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
    ((∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧
        ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ∧
      DifferentiableOn 𝕜 (iteratedDerivWithin n f s) s ∧ ContinuousOn (iteratedDerivWithin (n + 1) f s) s
⊢ ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s ↔ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s ∧ ContDiffOn 𝕜 1 (iteratedDerivWithin n f s) s

Tactic:
simp only [contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, hs,
    contDiffOn_one_iff_derivWithin, ← iteratedDerivWithin_succ]

Premises used: contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, contDiffOn_one_iff_derivWithin, iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ((∀ m ≤ n + 1, ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ m < n + 1, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
    ((∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧
        ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ∧
      DifferentiableOn 𝕜 (iteratedDerivWithin n f s) s ∧ ContinuousOn (iteratedDerivWithin (n + 1) f s) s

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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 = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1

Tactic:
rfl

Premises used: iteratedDeriv, rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
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
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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 =
    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:
rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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)
rw₃ rw₄ : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f) (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)

Tactic:
rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]

Premises used: iteratedDeriv_eq_equiv_comp, LinearIsometryEquiv.self_comp_symm, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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 → 𝕜
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)
⊢ (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)

Tactic:
rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]

Premises used: ContinuousMultilinearMap.map_smul_univ, iteratedDeriv_eq_iteratedFDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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 → 𝕜
⊢ 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:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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)
rw₂ 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)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDeriv 𝕜 n f x) = ‖iteratedDeriv n f x‖

Tactic:
rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, iteratedDeriv_eq_equiv_comp, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ∀ (x : 𝕜), iteratedDeriv 0 f x = f x
⊢ iteratedDeriv 0 f = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv 0 f x = f x

Tactic:
simp [iteratedDeriv]

Premises used: iteratedDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ∀ (x : 𝕜), iteratedDeriv 1 f x = deriv f x
⊢ iteratedDeriv 1 f = deriv f

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv 1 f x = deriv f x

Tactic:
simp [iteratedDeriv]

Premises used: iteratedDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
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 : ℕ),
        (↑m : ℕ∞) ≤ n →
          Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
              PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
            (iteratedDeriv m f)) ∧
      ∀ (m : ℕ), (↑m : ℕ∞) < n → Differentiable 𝕜 (iteratedDeriv m f)

Tactic:
simp only [contDiff_iff_continuous_differentiable, iteratedFDeriv_eq_equiv_comp,
    LinearIsometryEquiv.comp_continuous_iff, LinearIsometryEquiv.comp_differentiable_iff]

Premises used: contDiff_iff_continuous_differentiable, iteratedFDeriv_eq_equiv_comp, LinearIsometryEquiv.comp_differentiable_iff, LinearIsometryEquiv.comp_continuous_iff
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
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)
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) 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]

Premises used: contDiff_iff_iteratedDeriv, WithTop.coe_natCast
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ((∀ (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:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ∞
h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → Differentiable 𝕜 (iteratedDeriv m f)
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
contDiff_iff_iteratedDeriv.2 ⟨fun m hm => (h m hm).continuous, fun m hm => h m (le_of_lt hm)⟩

Premises used: Iff.mpr, le_of_lt, contDiff_iff_iteratedDeriv, And.intro, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ∞ω
m : ℕ
h : ContDiff 𝕜 n f
hmn : (↑m : ℕ∞ω) ≤ n
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (iteratedDeriv m f)

Tactic:
(contDiff_iff_iteratedDeriv.1 (h.of_le hmn)).1 m le_rfl

Premises used: le_rfl, contDiff_iff_iteratedDeriv, ContDiff.of_le, And.left, Iff.mp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
m : ℕ
h : ContDiff 𝕜 (↑m : ℕ∞ω) f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (iteratedDeriv m f)

Tactic:
ContDiff.continuous_iteratedDeriv m h (le_refl _)

Premises used: le_refl, ContDiff.continuous_iteratedDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ∞ω
m : ℕ
h : ContDiff 𝕜 n f
hmn : (↑m : ℕ∞ω) < n
⊢ Differentiable 𝕜 (iteratedDeriv m f)

Tactic:
(contDiff_iff_iteratedDeriv.1 (h.of_le (ENat.add_one_natCast_le_withTop_of_lt hmn))).2 m
    (mod_cast (lt_add_one m))

Premises used: ENat.add_one_natCast_le_withTop_of_lt, Nat.cast_lt._simp_1, lt_add_one, cast, contDiff_iff_iteratedDeriv, ContDiff.of_le, And.right, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
m : ℕ
h : ContDiff 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1) f
⊢ Differentiable 𝕜 (iteratedDeriv m f)

Tactic:
h.differentiable_iteratedDeriv m (Nat.cast_lt.mpr m.lt_succ_self)

Premises used: Iff.mpr, Nat.lt_succ_self, ContDiff.differentiable_iteratedDeriv, Nat.cast_lt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw : iteratedDerivWithin (n + 1) f univ = derivWithin (iteratedDerivWithin n f univ) univ
⊢ iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)

Tactic:
rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ]

Premises used: derivWithin_univ, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDerivWithin (n + 1) f univ = derivWithin (iteratedDerivWithin n f univ) univ

Tactic:
iteratedDerivWithin_succ

Premises used: iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDerivWithin (n + 1) f univ = derivWithin (iteratedDerivWithin n f univ) univ

Tactic:
exact iteratedDerivWithin_succ

Premises used: iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ∀ (x : 𝕜), iteratedDeriv n f x = deriv^[n] f x
⊢ iteratedDeriv n f = deriv^[n] f

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
h : iteratedDerivWithin n f univ x = deriv^[n] f x
⊢ iteratedDeriv n f x = deriv^[n] f x

Tactic:
rw [← iteratedDerivWithin_univ]

Premises used: iteratedDerivWithin_univ