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 ≠ ∞
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 :
  ∀ (y : E) (hy : y ∈ 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' y).unshift (f y) 1)) (v ∩ u) y
mpr₁ :
  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)
⊢ (∀ 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:
refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩
-- 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
y : E
hy : y ∈ v ∩ u
mpr :
  HasFDerivWithinAt f
    ((↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1))
    (v ∩ u) y
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (z : E) ↦
      (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f z))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1)) (v ∩ u) y

Tactic:
rw [← Function.comp_def _ f, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']

Premises used: LinearIsometryEquiv.comp_hasFDerivWithinAt_iff', Function.comp_def
-- 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
y : E
hy : y ∈ v ∩ u
⊢ HasFDerivWithinAt f (f' y) (v ∩ u) y

Tactic:
(f'_eq_deriv y hy.2).mono inter_subset_right

Premises used: And.right, HasFDerivWithinAt.mono, Set.inter_subset_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
y : E
hy : y ∈ v ∩ u
h :
  (↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) =
    f' y
⊢ HasFDerivWithinAt f
    ((↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1))
    (v ∩ u) y

Tactic:
convert! (f'_eq_deriv y hy.2).mono inter_subset_right

Premises used: And.right, HasFDerivWithinAt.mono, Set.inter_subset_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
y : E
hy : y ∈ v ∩ u
h :
  (↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) =
    ContinuousMultilinearMap.curry0 (p' y 0)
⊢ (↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) =
    f' y

Tactic:
rw [← Hp'.zero_eq y hy.1]

Premises used: HasFTaylorSeriesUpToOn.zero_eq, And.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 : ℕ∞ω
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
y : E
hy : y ∈ v ∩ u
h :
  ∀ (z : E),
    Eq.{uF + 1} (α := F)
      (((↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
              ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) :
            (a : E) → F)
          z :
        F)
      ((ContinuousMultilinearMap.curry0 (p' y 0) : (a : E) → F) z : F)
⊢ (↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) =
    ContinuousMultilinearMap.curry0 (p' y 0)

Tactic:
ext z
-- 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
y : E
hy : y ∈ v ∩ u
z : E
h :
  Eq.{uF + 1} (α := F)
    ((((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0 (last 0) : E) :
      F)
    (((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) z : F)
⊢ Eq.{uF + 1} (α := F)
    (((↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
            ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) :
          (a : E) → F)
        z :
      F)
    ((ContinuousMultilinearMap.curry0 (p' y 0) : (a : E) → F) z : F)

Tactic:
change ((p' y 0) (init (@cons 0 (fun _ => E) z 0))) (@cons 0 (fun _ => E) z 0 (last 0)) =
          ((p' y 0) 0) z

Premises used: Fin.cons, Fin.init, Fin.last, 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
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
y : E
hy : y ∈ v ∩ u
z : E
h :
  Eq.{uE + 1} (α := (i : Fin 0) → E)
    (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
        (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0) :
      (i : Fin 0) → E)
    (0 : (i : Fin 0) → E)
⊢ Eq.{uF + 1} (α := F)
    ((((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0 (last 0) : E) :
      F)
    (((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) z : F)

Tactic:
congr
-- 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
y : E
hy : y ∈ v ∩ u
z : E
⊢ Eq.{uE + 1} (α := (i : Fin 0) → E)
    (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
        (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0) :
      (i : Fin 0) → E)
    (0 : (i : Fin 0) → E)

Tactic:
norm_num [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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
⊢ HasFTaylorSeriesUpToOn n (fun (x : E) ↦ ContinuousMultilinearMap.curry0 (p' x 0)) p' (v ∩ u)

Tactic:
(Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1

Premises used: HasFTaylorSeriesUpToOn.zero_eq, HasFTaylorSeriesUpToOn.mono, Set.inter_subset_left, HasFTaylorSeriesUpToOn.congr, And.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 : ℕ∞ω
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
h :
  Eq (α := E → E →L[𝕜] F)
    (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) ↦ ContinuousMultilinearMap.curry0 (p' x 0)
h₁ : (fun (x : E) ↦ ((p' x).unshift (f x)).shift) = p'
⊢ 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:
convert! (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1

Premises used: HasFTaylorSeriesUpToOn.zero_eq, HasFTaylorSeriesUpToOn.mono, Set.inter_subset_left, HasFTaylorSeriesUpToOn.congr, And.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 : ℕ∞ω
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
h :
  ∀ (x y : E),
    Eq.{uF + 1} (α := F)
      ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                ((p' x).unshift (f x) 1) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F)
      ((ContinuousMultilinearMap.curry0 (p' x 0) : (a : E) → F) y : F)
⊢ Eq (α := E → E →L[𝕜] F)
    (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) ↦ ContinuousMultilinearMap.curry0 (p' x 0)

Tactic:
ext x y
-- 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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
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_1
v : Set E
hv : v ∈ 𝓝[insert x_1 u] x_1
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 y : E
h :
  Eq.{uF + 1} (α := F)
    ((((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin 1) ↦ E) (snoc (α := fun (x : Fin 1) ↦ E) 0 y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
⊢ Eq.{uF + 1} (α := F)
    ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
              ((p' x).unshift (f x) 1) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    ((ContinuousMultilinearMap.curry0 (p' x 0) : (a : E) → F) y : F)

Tactic:
change p' x 0 (init (@snoc 0 (fun _ : Fin 1 => E) 0 y)) y = p' x 0 0 y

Premises used: Fin.snoc, Fin.init, 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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
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_1
v : Set E
hv : v ∈ 𝓝[insert x_1 u] x_1
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 y : E
h h₁ :
  Eq.{uF + 1} (α := F) (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
    (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
⊢ Eq.{uF + 1} (α := F)
    ((((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin 1) ↦ E) (snoc (α := fun (x : Fin 1) ↦ E) 0 y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)

Tactic:
rw [init_snoc]

Premises used: Fin.init_snoc
-- 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
h :
  ∀ (x : E) (k : ℕ) (v : (i : Fin k) → E) (y : E),
    Eq.{uF + 1} (α := F)
      ((((((p' x).unshift (f x)).shift k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
⊢ (fun (x : E) ↦ ((p' x).unshift (f x)).shift) = p'

Tactic:
ext x k v y
-- 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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
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_1
v_1 : Set E
hv : v_1 ∈ 𝓝[insert x_1 u] x_1
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v_1
p'_an :
  n = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v_1
x : E
k : ℕ
v : (i : Fin k) → E
y : E
h :
  Eq.{uF + 1} (α := F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin k.succ) ↦ E) (snoc (α := fun (x : Fin k.succ) ↦ E) v y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (snoc (α := fun (x : Fin k.succ) ↦ E) v y (last k) : E) :
      F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
⊢ Eq.{uF + 1} (α := F)
    ((((((p' x).unshift (f x)).shift k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)

Tactic:
change p' x k (init (@snoc k (fun _ : Fin k.succ => E) v y))
            (@snoc k (fun _ : Fin k.succ => E) v y (last k)) = p' x k v y

Premises used: Fin.snoc, Fin.init, Fin.last, DFunLike.coe