awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
refine : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) s
⊢ ∃ u ∈ 𝓝[s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

Tactic:
refine ⟨s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
fderivWithin :
  ∀ (m_1 : ℕ),
    LT.lt (α := ℕ∞ω) (↑m_1 : ℕ∞ω) (↑m : ℕ∞ω) →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m_1) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m_1)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m_1.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m_1.succ))
          s x
cont :
  ∀ (m_1 : ℕ),
    LE.le (α := ℕ∞ω) (↑m_1 : ℕ∞ω) (↑m : ℕ∞ω) →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m_1) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m_1) s
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) s

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
y : E
zero_eq : y ∈ s → ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s y 0) = f y
⊢ y ∈ s → ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s y 0) = f y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
y : E
h : y ∈ s
⊢ ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s y 0) = f y

Tactic:
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
      iteratedFDerivWithin_zero_apply]

Premises used: ContinuousMultilinearMap.curry0_apply, ftaylorSeriesWithin, iteratedFDerivWithin_zero_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
k : ℕ
hk : LT.lt (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)
y : E
hy : y ∈ s
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ iteratedFDerivWithin 𝕜 k f s x) (fderivWithin 𝕜 (fun (x : E) ↦ iteratedFDerivWithin 𝕜 k f s x) s y) s
    y

Tactic:
(Hdiff k (lt_of_lt_of_le (mod_cast hk) (mod_cast hm)) y hy).hasFDerivWithinAt

Premises used: DifferentiableWithinAt.hasFDerivWithinAt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
k : ℕ
hk : LT.lt (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)
y : E
hy : y ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin k.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s y k.succ)) s y

Tactic:
convert! (Hdiff k (lt_of_lt_of_le (mod_cast hk) (mod_cast hm)) y hy).hasFDerivWithinAt

Premises used: DifferentiableWithinAt.hasFDerivWithinAt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
k : ℕ
hk : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k) s

Tactic:
Hcont k (le_trans (mod_cast hk) (mod_cast hm))

Premises used: ftaylorSeriesWithin, le_trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
k : ℕ
hk : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k) s

Tactic:
exact Hcont k (le_trans (mod_cast hk) (mod_cast hm))

Premises used: le_trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
h :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (iteratedFDerivWithin 𝕜 m f s) s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
contDiffOn_of_continuousOn_differentiableOn (fun m hm => (h m hm).continuousOn) fun m hm =>
    h m (le_of_lt hm)

Premises used: DifferentiableOn.continuousOn, contDiffOn_of_continuousOn_differentiableOn, le_of_lt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
suffices : ContDiffOn 𝕜 ω f s
⊢ ContDiffOn 𝕜 n f s

Tactic:
suffices ContDiffOn 𝕜 ω f s from this.of_le le_top
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_, ?_⟩

Premises used: Insert.insert, ftaylorSeriesWithin, self_mem_nhdsWithin, And.intro, Exists.intro, ContDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
refine_1 : HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
refine_2 :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
refine_1 : HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) s
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)

Tactic:
rw [insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
refine_1 : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
refine_1₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) ω →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
refine_1₂ :
  ∀ (m : ℕ),
    LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) ω →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) s
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) s

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
y : E
refine_1 : y ∈ s → ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s y 0) = f y
⊢ y ∈ s → ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s y 0) = f y

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
y : E
h_1 : y ∈ s
⊢ ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s y 0) = f y

Tactic:
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
        iteratedFDerivWithin_zero_apply]

Premises used: ContinuousMultilinearMap.curry0_apply, ftaylorSeriesWithin, iteratedFDerivWithin_zero_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
k : ℕ
refine_1 :
  LT.lt (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin k.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x k.succ)) s x
⊢ LT.lt (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin k.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x k.succ)) s x

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
k : ℕ
h_1 : LT.lt (α := ℕ∞ω) (↑k : ℕ∞ω) ω
y : E
hy : y ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin k.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s y k.succ)) s y

Tactic:
((h k).differentiableOn y hy).hasFDerivWithinAt

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, iteratedFDerivWithin, ContinuousMultilinearMap.curryLeft, MultilinearMap.mkContinuous, ftaylorSeriesWithin, Fin.induction, MultilinearMap.mk', Fin.cases, AnalyticOn.differentiableOn, MultilinearMap.mkContinuousLinear, Fin.tail, LinearMap.mkContinuous, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
k : ℕ
h_1 : LT.lt (α := ℕ∞ω) (↑k : ℕ∞ω) ω
y : E
hy : y ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin k.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s y k.succ)) s y

Tactic:
exact ((h k).differentiableOn y hy).hasFDerivWithinAt

Premises used: AnalyticOn.differentiableOn, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
k : ℕ
refine_1 :
  LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k) s
⊢ LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k) s

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
k : ℕ
h_1 : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k) s

Tactic:
(h k).continuousOn

Premises used: AnalyticOn.continuousOn, ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
k : ℕ
h_1 : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) ω
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x k) s

Tactic:
exact (h k).continuousOn

Premises used: AnalyticOn.continuousOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
i : ℕ
refine_2 :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) s
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)

Tactic:
rw [insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) s

Tactic:
h i

Premises used: ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) s

Tactic:
exact h i
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ω f s ↔ AnalyticOn 𝕜 f s

Tactic:
⟨fun h m ↦ h.analyticOn m, fun h ↦ h.contDiffOn hs⟩

Premises used: AnalyticOn.contDiffOn, ContDiffOn.analyticOn, Iff.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) ≤ n
hs : UniqueDiffOn 𝕜 s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s) s

Tactic:
((h.of_le hmn).ftaylorSeriesWithin hs).cont m le_rfl

Premises used: le_rfl, HasFTaylorSeriesUpToOn.cont, ftaylorSeriesWithin, ContDiffOn.of_le, ContDiffOn.ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ (↑(m + 1) : ℕ∞ω) ≤ n

Tactic:
have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hmn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
apply : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑(m + 1) : ℕ∞ω)
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
apply (((h.of_le this).ftaylorSeriesWithin hs).fderivWithin m ?_ x hx).differentiableWithinAt

Premises used: HasFTaylorSeriesUpToOn.fderivWithin, ContDiffOn.of_le, HasFDerivWithinAt.differentiableWithinAt, ContDiffOn.ftaylorSeriesWithin