awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
h₁ :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
      NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E)) →
    HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
        Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
        (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E)) →
      Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
          UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E)) →
        ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
            (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
                  F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
              F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
            ((continuousMultilinearCurryFin1 𝕜 E F :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
              (p x 1)) =
          ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0))
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (x : E) ↦ p x 0)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
        F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p x 1)))
    s x

Tactic:
convert! h.fderivWithin _ this x hx

Premises used: HasFTaylorSeriesUpToOn.fderivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
h₁ :
  ∀ (y : E) (v : (i : Fin 0) → E),
    Eq.{uF + 1} (α := F)
      ((((ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
                    (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
                          F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
                      F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
                    ((continuousMultilinearCurryFin1 𝕜 E F :
                        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                      (p x 1)) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
                y :
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) :
            (a : (i : Fin 0) → E) → F)
          v :
        F)
      ((((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0)) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
                y :
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) :
            (a : (i : Fin 0) → E) → F)
          v :
        F)
⊢ ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
        F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p x 1)) =
    ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0))

Tactic:
ext y v
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
h₁ :
  Eq.{uF + 1} (α := F) ((p x 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) 0 y) : F)
    ((p x 1 : (a : (i : Fin 1) → E) → F) (cons (α := fun (i : Fin 1) ↦ E) y v) : F)
⊢ Eq.{uF + 1} (α := F)
    ((((ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
                  (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
                        F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
                    F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
                  ((continuousMultilinearCurryFin1 𝕜 E F :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                    (p x 1)) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
              y :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        v :
      F)
    ((((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0)) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
              y :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        v :
      F)

Tactic:
change (p x 1) (snoc 0 y) = (p x 1) (cons y v)

Premises used: Fin.cons, Fin.snoc, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
h₁ :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y i : E) (cons (α := fun (i : Fin 1) ↦ E) y v i : E)
⊢ Eq.{uF + 1} (α := F) ((p x 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) 0 y) : F)
    ((p x 1 : (a : (i : Fin 1) → E) → F) (cons (α := fun (i : Fin 1) ↦ E) y v) : F)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h₁ :
  Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y default : E)
    (cons (α := fun (i : Fin 1) ↦ E) y v default : E)
⊢ Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y i : E) (cons (α := fun (i : Fin 1) ↦ E) y v i : E)

Tactic:
rw [Unique.eq_default (α := Fin 1) i]

Premises used: Unique.eq_default
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y default : E)
    (cons (α := fun (i : Fin 1) ↦ E) y v default : E)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun _x hx => (h.hasFDerivWithinAt hn hx).differentiableWithinAt

Premises used: HasFTaylorSeriesUpToOn.hasFDerivWithinAt, HasFDerivWithinAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : s ∈ 𝓝 x
⊢ HasFDerivAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    x

Tactic:
(h.hasFDerivWithinAt hn (mem_of_mem_nhds hx)).hasFDerivAt hx

Premises used: HasFTaylorSeriesUpToOn.hasFDerivWithinAt, mem_of_mem_nhds, HasFDerivWithinAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : s ∈ 𝓝 x
⊢ ∀ᶠ (y : E) in 𝓝 x,
    HasFDerivAt.{u, uE, uF} (𝕜 := 𝕜) f
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p y 1))
      y

Tactic:
(eventually_eventually_nhds.2 hx).mono fun _y hy => h.hasFDerivAt hn hy

Premises used: Iff.mpr, HasFTaylorSeriesUpToOn.hasFDerivAt, Filter.Eventually.mono, eventually_eventually_nhds
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : s ∈ 𝓝 x
⊢ DifferentiableAt 𝕜 f x

Tactic:
(h.hasFDerivAt hn hx).differentiableAt

Premises used: HasFTaylorSeriesUpToOn.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
mp :
  HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s →
    HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
      (∀ x ∈ s,
          HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
            (fun (y : E) ↦ p y n) (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s
            x) ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
          (fun (x : E) ↦ p x (n + 1)) s
mpr :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
      (∀ x ∈ s,
          HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
            (fun (y : E) ↦ p y n) (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s
            x) ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
          (fun (x : E) ↦ p x (n + 1)) s →
    HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s ↔
    HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
      (∀ x ∈ s,
          HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
            (fun (y : E) ↦ p y n) (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s
            x) ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
          (fun (x : E) ↦ p x (n + 1)) s

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s →
    HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
      (∀ x ∈ s,
          HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
            (fun (y : E) ↦ p y n) (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s
            x) ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
          (fun (x : E) ↦ p x (n + 1)) s

Tactic:
fun h ↦ ⟨h.of_le (mod_cast Nat.le_succ n),
      h.fderivWithin _ (mod_cast lt_add_one n), h.cont (n + 1) le_rfl⟩

Premises used: le_rfl, congrArg, Nat.cast_lt._simp_1, lt_add_one, Nat.cast_add._simp_1, HasFTaylorSeriesUpToOn.of_le, HasFTaylorSeriesUpToOn.cont, cast, Nat.le_succ, Nat.cast_le._simp_1, LE.le, Nat.cast, HasFTaylorSeriesUpToOn.fderivWithin, HAdd.hAdd, And.intro, LT.lt, OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s →
    HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
      (∀ x ∈ s,
          HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
            (fun (y : E) ↦ p y n) (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s
            x) ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
          (fun (x : E) ↦ p x (n + 1)) s

Tactic:
exact fun h ↦ ⟨h.of_le (mod_cast Nat.le_succ n),
      h.fderivWithin _ (mod_cast lt_add_one n), h.cont (n + 1) le_rfl⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
mpr : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
mpr₁ :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 →
      ∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
mpr₂ :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
⊢ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x

Tactic:
h.1.zero_eq

Premises used: HasFTaylorSeriesUpToOn.zero_eq, And.left
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
⊢ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x

Tactic:
exact h.1.zero_eq

Premises used: HasFTaylorSeriesUpToOn.zero_eq, And.left
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
pos :
  ∀ (h' : m < n),
    ∀ x ∈ s,
      HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
neg :
  ∀ (h' : ¬m < n),
    ∀ x ∈ s,
      HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
⊢ ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x

Tactic:
by_cases h' : m < n