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
f : E → F
x : E
n : ℕ
simp :
  (∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
⊢ (∃ u ∈ 𝓝[insert x univ] x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x

Tactic:
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem]

Premises used: nhdsWithin_univ, Set.insert_eq_of_mem, Set.mem_univ
-- 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
f : E → F
x : E
n : ℕ
mp :
  (∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) →
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
mpr :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x) →
    ∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
⊢ (∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x

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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
mp :
  ∀ (t : Set E) (htu : t ⊆ u) (ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (hxt : x ∈ t),
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
⊢ ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x

Tactic:
rcases mem_nhds_iff.mp H with ⟨t, htu, ht, hxt⟩

Premises used: mem_nhds_iff, 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
⊢ ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x

Tactic:
⟨f', ⟨t, ?_⟩, h_cont_diff.contDiffAt H⟩

Premises used: ContDiffWithinAt.contDiffAt, 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
mp : t ∈ 𝓝 x ∧ ∀ x ∈ t, HasFDerivAt f (f' x) x
⊢ ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x

Tactic:
refine ⟨f', ⟨t, ?_⟩, h_cont_diff.contDiffAt H⟩
-- 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
⊢ t ∈ 𝓝 x ∧ ∀ x ∈ t, HasFDerivAt f (f' x) x

Tactic:
⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩

Premises used: Iff.mpr, mem_nhds_iff, Set.Subset.rfl, 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
mp : ∀ x ∈ t, HasFDerivAt f (f' x) x
⊢ t ∈ 𝓝 x ∧ ∀ x ∈ t, HasFDerivAt f (f' x) x

Tactic:
refine ⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩
-- 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
y : E
hyt : y ∈ t
⊢ HasFDerivAt f (f' y) y

Tactic:
(h_fderiv y (htu hyt)).hasFDerivAt ?_

Premises used: HasFDerivWithinAt.hasFDerivAt
-- 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
y : E
hyt : y ∈ t
mp : u ∈ 𝓝 y
⊢ HasFDerivAt f (f' y) y

Tactic:
refine (h_fderiv y (htu hyt)).hasFDerivAt ?_

Premises used: HasFDerivWithinAt.hasFDerivAt
-- 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
y : E
hyt : y ∈ t
⊢ u ∈ 𝓝 y

Tactic:
mem_nhds_iff.mpr ⟨t, htu, ht, hyt⟩

Premises used: Iff.mpr, mem_nhds_iff, 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
y : E
hyt : y ∈ t
⊢ u ∈ 𝓝 y

Tactic:
exact mem_nhds_iff.mpr ⟨t, htu, ht, hyt⟩

Premises used: Iff.mpr, mem_nhds_iff, 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
f : E → F
x : E
n : ℕ
f' : E → E →L[𝕜] F
h_cont_diff : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
u : Set E
H : u ∈ 𝓝 x
h_fderiv : ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u

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
f : E → F
x : E
n : ℕ
f' : E → E →L[𝕜] F
h_cont_diff : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
u : Set E
H : u ∈ 𝓝 x
h_fderiv : ∀ x ∈ u, HasFDerivAt f (f' x) x
mpr : ∀ (x : E) (hxu : x ∈ u), HasFDerivWithinAt f (f' x) u x
⊢ ∃ u ∈ 𝓝 x,
    (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x

Tactic:
refine ⟨u, H, by simp, f', fun x hxu ↦ ?_, h_cont_diff.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
f : E → F
x_1 : E
n : ℕ
f' : E → E →L[𝕜] F
h_cont_diff : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x_1
u : Set E
H : u ∈ 𝓝 x_1
h_fderiv : ∀ x ∈ u, HasFDerivAt f (f' x) x
x : E
hxu : x ∈ u
⊢ HasFDerivWithinAt f (f' x) u x

Tactic:
(h_fderiv x hxu).hasFDerivWithinAt

Premises used: HasFDerivAt.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
f : E → F
x_1 : E
n : ℕ
f' : E → E →L[𝕜] F
h_cont_diff : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x_1
u : Set E
H : u ∈ 𝓝 x_1
h_fderiv : ∀ x ∈ u, HasFDerivAt f (f' x) x
x : E
hxu : x ∈ u
⊢ HasFDerivWithinAt f (f' x) u x

Tactic:
exact (h_fderiv x hxu).hasFDerivWithinAt

Premises used: HasFDerivAt.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
f : E → F
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
h' : n ≠ ∞
⊢ ∀ᶠ (y : E) in 𝓝 x, ContDiffAt 𝕜 n f y

Tactic:
simpa [nhdsWithin_univ] using ContDiffWithinAt.eventually h h'

Premises used: ContDiffWithinAt.eventually, nhdsWithin_univ
-- 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
rw :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDeriv 𝕜 n f x)

Tactic:
rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
⊢ Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ∞ → Eq (α := ℕ∞ω) (↑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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
rcases :
  ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
    (hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
      (iteratedFDerivWithin 𝕜 n f univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩

Premises used: le_rfl, 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
rw :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
rw [← iteratedFDerivWithin_inter_open u_open xu,
    ← iteratedFDerivWithin_inter_open u_open xu (s := univ)]

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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
st : s ∩ u ⊆ univ ∩ u
hs₁ : UniqueDiffOn 𝕜 (s ∩ u)
ht : UniqueDiffOn 𝕜 (univ ∩ u)
h₁ : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (univ ∩ u)
hx₁ : x ∈ s ∩ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)

Tactic:
apply iteratedFDerivWithin_subset

Premises used: iteratedFDerivWithin_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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ s ∩ u ⊆ univ ∩ u

Tactic:
inter_subset_inter_left _ (subset_univ _)

Premises used: Set.subset_univ, Set.inter_subset_inter_left
-- 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ s ∩ u ⊆ univ ∩ u

Tactic:
exact inter_subset_inter_left _ (subset_univ _)

Premises used: Set.subset_univ, Set.inter_subset_inter_left
-- 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (s ∩ u)

Tactic:
hs.inter u_open

Premises used: 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (s ∩ u)

Tactic:
exact hs.inter u_open

Premises used: 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (univ ∩ u)

Tactic:
apply uniqueDiffOn_univ.inter u_open

Premises used: uniqueDiffOn_univ, 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f (univ ∩ u)

Tactic:
simpa using hu
-- 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ x ∈ s ∩ u

Tactic:
⟨hx, xu⟩

Premises used: Set.Mem, setOf, Set.inter, And.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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ x ∈ s ∩ u

Tactic:
exact ⟨hx, xu⟩
-- 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
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f f'
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
⟨f', hf⟩

Premises used: ContDiff, 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
f : E → F
n : ℕ∞ω
⊢ ContDiffOn 𝕜 n f ∅

Tactic:
fun _x hx ↦ hx.elim

Premises used: False.elim, 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
f : E → F
n : ℕ∞ω
mp : ContDiffOn 𝕜 ω f univ → ContDiff 𝕜 ω f
mpr : ContDiff 𝕜 ω f → ContDiffOn 𝕜 ω f univ
⊢ ContDiffOn 𝕜 ω f univ ↔ ContDiff 𝕜 ω f

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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
h :
  HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
⊢ ContDiff 𝕜 ω f

Tactic:
use ftaylorSeriesWithin 𝕜 f univ

Premises used: Set.univ, 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
h :
  HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
⊢ HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff]

Premises used: hasFTaylorSeriesUpToOn_univ_iff
-- 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩

Premises used: uniqueDiffOn_univ, And.intro, 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
h :
  ∀ (i : ℕ),
    AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
i : ℕ
h :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
rw [← analyticOn_univ]

Premises used: analyticOn_univ