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
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (n + 1) f p u
H'p :
  n + 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
Hp₁ :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
⊢ n + 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u

Tactic:
rw [hasFTaylorSeriesUpToOn_succ_iff_right] at Hp

Premises used: hasFTaylorSeriesUpToOn_succ_iff_right
-- 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
H'p :
  n + 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
      (fun (y : E) ↦
        (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
          (p y 1))
      (fun (y : E) ↦ (p y).shift) u ∧
    (n = ω →
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
          (fun (x : E) ↦ (fun (y : E) ↦ (p y).shift) x i) u)

Tactic:
⟨Hp.2.2, ?_⟩

Premises used: And.right, 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
H'p :
  n + 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
mp :
  n = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
        (fun (x : E) ↦ (fun (y : E) ↦ (p y).shift) x i) u
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
      (fun (y : E) ↦
        (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
          (p y 1))
      (fun (y : E) ↦ (p y).shift) u ∧
    (n = ω →
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
          (fun (x : E) ↦ (fun (y : E) ↦ (p y).shift) x i) u)

Tactic:
refine ⟨Hp.2.2, ?_⟩
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : Ne (α := ℕ∞ω) ω ∞
h'n : HAdd.hAdd (α := ℕ∞ω) ω 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s x
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) ω
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
H'p :
  HAdd.hAdd (α := ℕ∞ω) ω 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
mp :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
    (fun (x : E) ↦
      (continuousMultilinearCurryRightEquiv' 𝕜 i E F :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i.succ) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
        (p x (i + 1)))
    u
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
    (fun (x : E) ↦ (fun (y : E) ↦ (p y).shift) x i) u

Tactic:
change AnalyticOn 𝕜
        (fun x ↦ (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u

Premises used: AnalyticOn, continuousMultilinearCurryRightEquiv', HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : Ne (α := ℕ∞ω) ω ∞
h'n : HAdd.hAdd (α := ℕ∞ω) ω 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s x
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) ω
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
H'p :
  HAdd.hAdd (α := ℕ∞ω) ω 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
apply :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i.succ) ↦ E) F) (fun (x : E) ↦ p x (i + 1))
    u
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
    (fun (x : E) ↦
      (continuousMultilinearCurryRightEquiv' 𝕜 i E F :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i.succ) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
        (p x (i + 1)))
    u

Tactic:
apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn
        ?_ (Set.mapsTo_univ _ _)

Premises used: LinearIsometryEquiv.analyticOnNhd, Set.mapsTo_univ, AnalyticOnNhd.comp_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
x : E
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : Ne (α := ℕ∞ω) ω ∞
h'n : HAdd.hAdd (α := ℕ∞ω) ω 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s x
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) ω
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
H'p :
  HAdd.hAdd (α := ℕ∞ω) ω 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i.succ) ↦ E) F) (fun (x : E) ↦ p x (i + 1))
    u

Tactic:
H'p rfl _

Premises used: rfl
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : Ne (α := ℕ∞ω) ω ∞
h'n : HAdd.hAdd (α := ℕ∞ω) ω 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s x
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) ω
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            (p x 1))
        (fun (x : E) ↦ (p x).shift) u
H'p :
  HAdd.hAdd (α := ℕ∞ω) ω 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i.succ) ↦ E) F) (fun (x : E) ↦ p x (i + 1))
    u

Tactic:
exact H'p rfl _

Premises used: rfl
-- 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
mpr :
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
rw [contDiffWithinAt_iff_of_ne_infty h'n]

Premises used: contDiffWithinAt_iff_of_ne_infty
-- 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
mpr :
  ∀ (v : Set E) (hv : v ∈ 𝓝[insert x u] x) (p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F))
    (Hp' : HasFTaylorSeriesUpToOn n f' p' v)
    (p'_an :
      n = ω →
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v),
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
        HasFTaylorSeriesUpToOn (n + 1) f p u ∧
          (n + 1 = ω →
            ∀ (i : ℕ),
              AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
                (fun (x : E) ↦ p x i) u)
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)

Tactic:
rcases (contDiffWithinAt_iff_of_ne_infty hn).1 Hf' with ⟨v, hv, p', Hp', p'_an⟩

Premises used: contDiffWithinAt_iff_of_ne_infty, 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
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)

Tactic:
⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩

Premises used: Inter.inter, And.intro, Exists.intro, FormalMultilinearSeries.unshift
-- 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
mpr : v ∩ u ∈ 𝓝[insert x s] x
mpr₁ : HasFTaylorSeriesUpToOn.{u, uE, uF} (𝕜 := 𝕜) (n + 1) f (fun (x : E) ↦ (p' x).unshift (f x)) (v ∩ u)
mpr₂ :
  n + 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ (fun (x : E) ↦ (p' x).unshift (f x)) x i) (v ∩ u)
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)

Tactic:
refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩
-- 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
apply : v ∈ 𝓝[insert x s] x
⊢ v ∩ u ∈ 𝓝[insert x s] x

Tactic:
apply Filter.inter_mem _ hu

Premises used: Filter.inter_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
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
a : v ∈ 𝓝[u] x
⊢ v ∈ 𝓝[insert x s] x

Tactic:
apply nhdsWithin_le_of_mem hu

Premises used: nhdsWithin_le_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
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ v ∈ 𝓝[u] x

Tactic:
nhdsWithin_mono _ (subset_insert x u) hv

Premises used: Set.subset_insert, nhdsWithin_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
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ v ∈ 𝓝[u] x

Tactic:
exact nhdsWithin_mono _ (subset_insert x u) hv

Premises used: Set.subset_insert, nhdsWithin_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
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
mpr :
  (∀ x ∈ v ∩ u, ContinuousMultilinearMap.curry0 ((p' x).unshift (f x) 0) = f x) ∧
    (∀ x ∈ v ∩ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
          (fun (y : E) ↦ (p' y).unshift (f y) 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' x).unshift (f x) 1)) (v ∩ u) x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            ((p' x).unshift (f x) 1))
        (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
⊢ HasFTaylorSeriesUpToOn.{u, uE, uF} (𝕜 := 𝕜) (n + 1) f (fun (x : E) ↦ (p' x).unshift (f x)) (v ∩ u)

Tactic:
rw [hasFTaylorSeriesUpToOn_succ_iff_right]

Premises used: hasFTaylorSeriesUpToOn_succ_iff_right
-- 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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ (∀ x ∈ v ∩ u, ContinuousMultilinearMap.curry0 ((p' x).unshift (f x) 0) = f x) ∧
    (∀ x ∈ v ∩ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
          (fun (y : E) ↦ (p' y).unshift (f y) 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' x).unshift (f x) 1)) (v ∩ u) x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) n
        (fun (x : E) ↦
          (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            ((p' x).unshift (f x) 1))
        (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)

Tactic:
⟨fun y _ => rfl, fun y hy => ?_, ?_⟩

Premises used: And.intro, rfl