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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
fderivWithin :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
    (Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u),
    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
⊢ 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

Tactic:
rcases (h x hx).of_le this _ le_rfl with ⟨u, hu, p, Hp⟩

Premises used: le_rfl, ContDiffWithinAt.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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
fderivWithin :
  ∀ (hu : u ∈ 𝓝[s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u),
    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
⊢ 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

Tactic:
rw [insert_eq_of_mem hx] at hu

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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
fderivWithin :
  ∀ (o : Set E) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o) (xo : x ∈ o) (ho : o ∩ s ⊆ u),
    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
⊢ 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

Tactic:
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩

Premises used: mem_nhdsWithin, Iff.mp
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ s ⊆ u
⊢ s ∩ o ⊆ u

Tactic:
rw [inter_comm] at ho

Premises used: Set.inter_comm
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
rw :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (iteratedFDerivWithin 𝕜 m.succ f (s ∩ o) x)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (iteratedFDerivWithin 𝕜 m.succ f s x)

Tactic:
rw [← iteratedFDerivWithin_inter_open o_open xo]

Premises used: iteratedFDerivWithin_inter_open
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (iteratedFDerivWithin 𝕜 m.succ f (s ∩ o) x)

Tactic:
(Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩

Premises used: le_rfl, HasFTaylorSeriesUpToOn.mono, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, UniqueDiffOn.inter
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (iteratedFDerivWithin 𝕜 m.succ f (s ∩ o) x)

Tactic:
exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩

Premises used: le_rfl, HasFTaylorSeriesUpToOn.mono, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, UniqueDiffOn.inter
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)

Tactic:
have : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ := by
      change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x
      rw [← iteratedFDerivWithin_inter_open o_open xo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
fderivWithin :
  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) (p x m.succ)) (s ∩ o) x
⊢ 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

Tactic:
rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)]

Premises used: IsOpen.mem_nhds, hasFDerivWithinAt_inter
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
y : E
hy : y ∈ s
yo : y ∈ o
rw : p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y

Tactic:
rw [← iteratedFDerivWithin_inter_open o_open yo]

Premises used: iteratedFDerivWithin_inter_open
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

Tactic:
(Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
          (hs.inter o_open) ⟨hy, yo⟩

Premises used: cast, HasFTaylorSeriesUpToOn.mono, Nat.le_succ, Nat.cast_le._simp_1, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, UniqueDiffOn.inter, Eq.symm
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

Tactic:
exact
        (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
          (hs.inter o_open) ⟨hy, yo⟩

Premises used: HasFTaylorSeriesUpToOn.mono, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, UniqueDiffOn.inter
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
⊢ ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m

Tactic:
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin 𝕜 m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact
        (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
          (hs.inter o_open) ⟨hy, yo⟩
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ 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) (p x m.succ)) (s ∩ o) x

Tactic:
((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr
        (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm

Premises used: Nat.cast_lt._simp_1, lt_add_one, cast, HasFTaylorSeriesUpToOn.mono, HasFTaylorSeriesUpToOn.fderivWithin, And.intro, HasFDerivWithinAt.congr, Eq.symm
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ 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) (p x m.succ)) (s ∩ o) x

Tactic:
exact
      ((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr
        (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm

Premises used: Nat.cast_lt._simp_1, lt_add_one, cast, HasFTaylorSeriesUpToOn.mono, HasFTaylorSeriesUpToOn.fderivWithin, And.intro, HasFDerivWithinAt.congr, Eq.symm
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
cont :
  ∀ x ∈ s,
    ∃ (t : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
        x ∈ t ∧
          ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
            (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) s

Tactic:
apply continuousOn_of_locally_continuousOn

Premises used: continuousOn_of_locally_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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
cont :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
    (Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
    ∃ (t : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
        x ∈ t ∧
          ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
            (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
rcases (h x hx).of_le hm _ le_rfl with ⟨u, hu, p, Hp⟩

Premises used: le_rfl, ContDiffWithinAt.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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
cont :
  ∀ (o : Set E) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o) (xo : x ∈ o)
    (ho : o ∩ insert x s ⊆ u),
    ∃ (t : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
        x ∈ t ∧
          ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
            (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩

Premises used: mem_nhdsWithin, Iff.mp
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ insert x s ⊆ u
⊢ o ∩ s ⊆ u

Tactic:
rw [insert_eq_of_mem hx] at ho

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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ s ⊆ u
⊢ s ∩ o ⊆ u

Tactic:
rw [inter_comm] at ho

Premises used: Set.inter_comm
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
⟨o, o_open, xo, ?_⟩

Premises used: And.intro, Exists.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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
cont :
  ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
refine ⟨o, o_open, xo, ?_⟩
-- 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
y : E
hy : y ∈ s
yo : y ∈ o
rw : p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y

Tactic:
rw [← iteratedFDerivWithin_inter_open o_open yo]

Premises used: iteratedFDerivWithin_inter_open