awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hr :
  0 <
    FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜))
hs :
  AnalyticOn 𝕜 f
    (Metric.eball x
      (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
        (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜))))
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
    (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := 𝕜)
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)))

Tactic:
exact hs.hasFPowerSeriesOnSubball hr le_rfl

Premises used: le_rfl, AnalyticOn.hasFPowerSeriesOnSubball
-- 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 : 𝕜), iteratedDerivWithin n f univ x = iteratedDeriv n f x
⊢ iteratedDerivWithin n f univ = iteratedDeriv 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 : ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
h₁ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ 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)
h₂ h₃ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDeriv 𝕜 n f 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)
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x

Tactic:
rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]

Premises used: iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_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
s : Set 𝕜
x : 𝕜
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
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)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDeriv 𝕜 n f 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)
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x

Tactic:
rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_eq_iteratedFDeriv hs h hx]

Premises used: iteratedFDerivWithin_eq_iteratedFDeriv, iteratedDerivWithin, 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
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1

Tactic:
rfl

Premises used: iteratedDerivWithin, 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
s : Set 𝕜
h :
  ∀ (x : 𝕜),
    iteratedDerivWithin n f s 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)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x
⊢ iteratedDerivWithin n f s =
    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)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → 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
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s 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)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → 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
s : Set 𝕜
rw :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (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)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)))
rw₁ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (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)
      (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F))
rw₂ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (id ∘ iteratedFDerivWithin 𝕜 n f s)
rw₃ rw₄ :
  Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    (iteratedFDerivWithin 𝕜 n f s)
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s)
    ((⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) ∘
      iteratedDerivWithin n f s)

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

Premises used: LinearIsometryEquiv.self_comp_symm, iteratedDerivWithin_eq_equiv_comp, 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
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
rw :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) m : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (i : Fin n) ↦ HSMul.hSMul (β := 𝕜) (m i) 1 : F)
⊢ (iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) m =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ i : Fin n, m i) (iteratedDerivWithin n f s x)

Tactic:
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← ContinuousMultilinearMap.map_smul_univ]

Premises used: ContinuousMultilinearMap.map_smul_univ, iteratedDerivWithin_eq_iteratedFDerivWithin
-- 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 : 𝕜
m : Fin n → 𝕜
⊢ Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) m : F)
    ((iteratedFDerivWithin 𝕜 n f s 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
s : Set 𝕜
x : 𝕜
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s 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)
        (iteratedFDerivWithin 𝕜 n f s : 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    norm.{u_2} (E := F)
      ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) :
            (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F) → F)
          (iteratedFDerivWithin 𝕜 n f s x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
        F)
rw₂ rw₃ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ 𝕜) F)
      (iteratedFDerivWithin 𝕜 n f s x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x) =
    ‖iteratedDerivWithin n f s x‖

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

Premises used: LinearIsometryEquiv.norm_map, iteratedDerivWithin_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
s : Set 𝕜
h : ∀ (x : 𝕜), iteratedDerivWithin 0 f s x = f x
⊢ iteratedDerivWithin 0 f s = 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
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 0 f s x = f x

Tactic:
simp [iteratedDerivWithin]

Premises used: iteratedDerivWithin
-- 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 𝕜
h : ∀ (x : 𝕜), iteratedDerivWithin 1 f s x = derivWithin f s x
⊢ iteratedDerivWithin 1 f s = derivWithin f 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
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
pos : ∀ (hsx : AccPt x (𝓟 s)), iteratedDerivWithin 1 f s x = derivWithin f s x
neg : ∀ (hsx : ¬AccPt x (𝓟 s)), iteratedDerivWithin 1 f s x = derivWithin f s x
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

Tactic:
by_cases hsx : AccPt x (𝓟 s)

Premises used: Filter.principal, 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
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hsx : AccPt x (𝓟 s)
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

Tactic:
simp only [iteratedDerivWithin, iteratedFDerivWithin_one_apply hsx.uniqueDiffWithinAt,
      derivWithin]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_one_apply, derivWithin, AccPt.uniqueDiffWithinAt
-- 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 𝕜
x : 𝕜
hsx : ¬AccPt x (𝓟 s)
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

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

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
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContinuousOn.{u_1, u_2} (Y := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hdiff :
  ∀ (m : ℕ), (↑m : ℕ∞) < n → DifferentiableOn.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hcont₁ :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
        (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff₁ :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
        (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
apply contDiffOn_of_continuousOn_differentiableOn

Premises used: contDiffOn_of_continuousOn_differentiableOn
-- 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 : ℕ∞
Hcont : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContinuousOn.{u_1, u_2} (Y := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hdiff :
  ∀ (m : ℕ), (↑m : ℕ∞) < n → DifferentiableOn.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
        (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff]

Premises used: iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_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
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContinuousOn.{u_1, u_2} (Y := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
Hdiff :
  ∀ (m : ℕ), (↑m : ℕ∞) < n → DifferentiableOn.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F)
        (fun (x : 𝕜) ↦ iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]

Premises used: iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_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
s : Set 𝕜
n : ℕ∞
h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
h₁ :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 m f s) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
apply contDiffOn_of_differentiableOn

Premises used: contDiffOn_of_differentiableOn
-- 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 : ℕ∞
h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 m f s) s

Tactic:
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]

Premises used: iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_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
s : Set 𝕜
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) ≤ n
hs : UniqueDiffOn 𝕜 s
⊢ ContinuousOn (iteratedDerivWithin m f s) s

Tactic:
simpa only [iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff] using
    h.continuousOn_iteratedFDerivWithin hmn hs

Premises used: ContDiffOn.continuousOn_iteratedFDerivWithin, iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_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
s : Set 𝕜
x : 𝕜
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x

Tactic:
simpa only [iteratedDerivWithin_eq_equiv_comp,
    LinearIsometryEquiv.comp_differentiableWithinAt_iff] using
    h.differentiableWithinAt_iteratedFDerivWithin hmn hs

Premises used: LinearIsometryEquiv.comp_differentiableWithinAt_iff, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, iteratedDerivWithin_eq_equiv_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
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 s
x : 𝕜
hx : x ∈ s
rwa rwa₁ rwa₂ rwa₃ : UniqueDiffOn 𝕜 s
⊢ UniqueDiffOn 𝕜 (insert x s)

Tactic:
rwa [insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- 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
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s ↔
    (∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), (↑m : ℕ∞) < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Tactic:
simp only [contDiffOn_iff_continuousOn_differentiableOn hs, iteratedFDerivWithin_eq_equiv_comp,
    LinearIsometryEquiv.comp_continuousOn_iff, LinearIsometryEquiv.comp_differentiableOn_iff]

Premises used: contDiffOn_iff_continuousOn_differentiableOn, iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff, LinearIsometryEquiv.comp_continuousOn_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
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
rw :
  ((∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Tactic:
rw [show n = ((n : ℕ∞) : ℕ∞ω) from rfl,
    contDiffOn_iff_continuousOn_differentiableOn_deriv hs]

Premises used: contDiffOn_iff_continuousOn_differentiableOn_deriv, 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
⊢ ((∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

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 𝕜
h : ∀ (x : 𝕜), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) f s = derivWithin (iteratedDerivWithin n 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 : 𝕜
pos : ∀ (hxs : AccPt x (𝓟 s)), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
neg : ∀ (hxs : ¬AccPt x (𝓟 s)), iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
by_cases hxs : AccPt x (𝓟 s)

Premises used: Filter.principal, 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 : 𝕜
hxs : AccPt x (𝓟 s)
pos :
  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)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
      iteratedFDerivWithin_eq_equiv_comp,
      LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt, derivWithin]

Premises used: LinearIsometryEquiv.comp_fderivWithin, iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_eq_equiv_comp, iteratedFDerivWithin_succ_apply_left, derivWithin, AccPt.uniqueDiffWithinAt