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
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
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

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

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
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
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

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

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
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 ∈ 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 le_rfl (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
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
A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)

Tactic:
((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm

Premises used: le_rfl, HasFTaylorSeriesUpToOn.cont, HasFTaylorSeriesUpToOn.mono, ContinuousOn.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
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
A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)

Tactic:
exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm

Premises used: le_rfl, HasFTaylorSeriesUpToOn.cont, HasFTaylorSeriesUpToOn.mono, ContinuousOn.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 t : Set E
f : E → F
x : E
n : ℕ
st : s ⊆ t
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
h : ContDiffOn 𝕜 (↑n : ℕ∞ω) f t
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f t x)

Tactic:
(((h.ftaylorSeriesWithin ht).mono st).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hs hx).symm

Premises used: le_rfl, HasFTaylorSeriesUpToOn.mono, ftaylorSeriesWithin, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, Eq.symm, 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω

Tactic:
simp
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
rcases :
  ∀ (U : Set E) (hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (haU : a ∈ U)
    (hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)),
    ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t

Tactic:
rcases h.contDiffOn' hm (by simp) with ⟨U, hUo, haU, hfU⟩

Premises used: ContDiffWithinAt.contDiffOn'
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
rw : s ∩ U ∈ 𝓝[s] a
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U

Tactic:
rw [eventually_smallSets_subset]

Premises used: Filter.eventually_smallSets_subset
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
⊢ s ∩ U ∈ 𝓝[s] a

Tactic:
inter_mem_nhdsWithin _ <| hUo.mem_nhds haU

Premises used: inter_mem_nhdsWithin, IsOpen.mem_nhds
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
⊢ s ∩ U ∈ 𝓝[s] a

Tactic:
exact inter_mem_nhdsWithin _ <| hUo.mem_nhds haU

Premises used: inter_mem_nhdsWithin, IsOpen.mem_nhds
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U

Tactic:
have : ∀ᶠ t in (𝓝[s] a).smallSets, t ⊆ s ∩ U := by
    rw [eventually_smallSets_subset]
    exact inter_mem_nhdsWithin _ <| hUo.mem_nhds haU
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t

Tactic:
this.mono fun t ht ↦ .mono ?_ ht

Premises used: HasFTaylorSeriesUpToOn.mono, Filter.Eventually.mono
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
refine : ∀ (t : Set E) (ht : t ⊆ s ∩ U), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t

Tactic:
refine this.mono fun t ht ↦ .mono ?_ ht

Premises used: Filter.Eventually.mono
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
rw :
  ∀ (hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)) (this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U) (t : Set E)
    (ht : t ⊆ s ∩ U), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)

Tactic:
rw [insert_eq_of_mem ha] at hfU

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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)

Tactic:
(hfU.ftaylorSeriesWithin (hs.inter hUo)).congr_series fun k hk x hx ↦ ?_

Premises used: UniqueDiffOn.inter, HasFTaylorSeriesUpToOn.congr_series, 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
refine :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)) (x : E) (hx : x ∈ s ∩ U),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((fun (x : E) ↦
          (ftaylorSeriesWithin 𝕜 f (s ∩ U) x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
        x)
      ((fun (x : E) ↦
          (ftaylorSeriesWithin 𝕜 f s x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
        x)
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)

Tactic:
refine (hfU.ftaylorSeriesWithin (hs.inter hUo)).congr_series fun k hk x hx ↦ ?_

Premises used: UniqueDiffOn.inter, HasFTaylorSeriesUpToOn.congr_series, 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
k : ℕ
hk : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)
x : E
hx : x ∈ s ∩ U
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((fun (x : E) ↦
        (ftaylorSeriesWithin 𝕜 f (s ∩ U) x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)
    ((fun (x : E) ↦ (ftaylorSeriesWithin 𝕜 f s x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)

Tactic:
iteratedFDerivWithin_inter_open hUo hx.2

Premises used: ftaylorSeriesWithin, And.right, 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
k : ℕ
hk : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)
x : E
hx : x ∈ s ∩ U
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((fun (x : E) ↦
        (ftaylorSeriesWithin 𝕜 f (s ∩ U) x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)
    ((fun (x : E) ↦ (ftaylorSeriesWithin 𝕜 f s x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)

Tactic:
exact iteratedFDerivWithin_inter_open hUo hx.2

Premises used: And.right, 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
rcases :
  ∀ (p : E → FormalMultilinearSeries 𝕜 E F)
    (hp :
      HasFTaylorSeriesUpToOn ω f p s ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
            s),
    ContDiffOn 𝕜 ω f s
⊢ ContDiffOn 𝕜 ω f s

Tactic:
rcases h.exists_hasFTaylorSeriesUpToOn hs with ⟨p, hp⟩

Premises used: AnalyticOn.exists_hasFTaylorSeriesUpToOn
-- 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
⟨s, ?_, p, hp⟩

Premises used: 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
refine : s ∈ 𝓝[insert x s] x
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
refine ⟨s, ?_, p, hp⟩
-- 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
rw : s ∈ 𝓝[s] x
⊢ s ∈ 𝓝[insert x s] x

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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[s] x

Tactic:
self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[s] x

Tactic:
exact self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- 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 : AnalyticOnNhd 𝕜 f s
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 n f s

Tactic:
h.analyticOn.contDiffOn hs

Premises used: AnalyticOn.contDiffOn, AnalyticOnNhd.analyticOn
-- 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 : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticOn 𝕜 f s
⊢ ContDiffOn 𝕜 n f s

Tactic:
fun x hx ↦ (h x hx).contDiffWithinAt

Premises used: AnalyticWithinAt.contDiffWithinAt, ContDiffOn
-- 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 : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ ContDiffOn 𝕜 n f s

Tactic:
h.analyticOn.contDiffOn_of_completeSpace

Premises used: AnalyticOnNhd.analyticOn, AnalyticOn.contDiffOn_of_completeSpace
-- 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
rw : ∃ u ∈ 𝓝[s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

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 : ℕ∞
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
⊢ ∃ u ∈ 𝓝[s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

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

Premises used: ftaylorSeriesWithin, self_mem_nhdsWithin, And.intro, Exists.intro