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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
refine_1 :
  (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s x) ∧
      ∀ (n : ℕ),
        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) s
⊢ (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s

Tactic:
rw [hasFTaylorSeriesUpToOn_top_iff hN]

Premises used: hasFTaylorSeriesUpToOn_top_iff
-- 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
hN : ∞ ≤ N
h : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
⊢ (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s x) ∧
      ∀ (n : ℕ),
        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) s

Tactic:
⟨(hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).1,
      (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).2.1,
      fun n ↦ (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h n)).2.2⟩

Premises used: hasFTaylorSeriesUpToOn_succ_nat_iff_right, And.right, And.left, And.intro, Iff.mp, OfNat.ofNat
-- 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
hN : ∞ ≤ N
h : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
⊢ (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s x) ∧
      ∀ (n : ℕ),
        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) s

Tactic:
exact ⟨(hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).1,
      (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).2.1,
      fun n ↦ (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h n)).2.2⟩
-- 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
hN : ∞ ≤ N
h :
  (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s
apply : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
⊢ HasFTaylorSeriesUpToOn N f p s

Tactic:
apply (hasFTaylorSeriesUpToOn_top_iff_add hN 1).2 (fun n ↦ ?_)

Premises used: Iff.mpr, OfNat.ofNat, hasFTaylorSeriesUpToOn_top_iff_add
-- 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
hN : ∞ ≤ N
h :
  (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s
n : ℕ
rw :
  (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s
⊢ HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s

Tactic:
rw [hasFTaylorSeriesUpToOn_succ_nat_iff_right]

Premises used: hasFTaylorSeriesUpToOn_succ_nat_iff_right
-- 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
hN : ∞ ≤ N
h :
  (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s
n : ℕ
⊢ (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s

Tactic:
⟨h.1, h.2.1, (h.2.2).of_le (m := n) (natCast_le_of_coe_top_le_withTop hN n)⟩

Premises used: ENat.natCast_le_of_coe_top_le_withTop, HasFTaylorSeriesUpToOn.of_le, And.right, And.left, And.intro
-- 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
hN : ∞ ≤ N
h :
  (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s
n : ℕ
⊢ (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ s,
        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)) s 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) s

Tactic:
exact ⟨h.1, h.2.1, (h.2.2).of_le (m := n) (natCast_le_of_coe_top_le_withTop hN n)⟩
-- 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
⊢ ∞ ≤ HAdd.hAdd (α := ℕ∞ω) ω 1

Tactic:
simp
-- 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
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) ω 1) f p s ↔
    (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      (∀ x ∈ s,
          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)) s 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) s

Tactic:
exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)

Premises used: hasFTaylorSeriesUpToOn_top_iff_right
-- 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
⊢ ∞ ≤ HAdd.hAdd (α := ℕ∞ω) ∞ 1

Tactic:
simp
-- 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
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) ∞ 1) f p s ↔
    (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      (∀ x ∈ s,
          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)) s 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) s

Tactic:
exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)

Premises used: hasFTaylorSeriesUpToOn_top_iff_right
-- 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_1 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s ↔
    (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      (∀ x ∈ s,
          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)) s 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) s

Tactic:
hasFTaylorSeriesUpToOn_succ_nat_iff_right

Premises used: WithTop.map₂, hasFTaylorSeriesUpToOn_succ_nat_iff_right, WithTop.some, Option.map₂
-- 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_1 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s ↔
    (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      (∀ x ∈ s,
          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)) s 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) s

Tactic:
exact hasFTaylorSeriesUpToOn_succ_nat_iff_right

Premises used: hasFTaylorSeriesUpToOn_succ_nat_iff_right
-- 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
⊢ HasFTaylorSeriesUpToOn (n + 1) f p s ↔
    (∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      (∀ x ∈ s,
          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)) s 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) s

Tactic:
match n with
  | ⊤ => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
  | (⊤ : ℕ∞) => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
  | (n : ℕ) => exact hasFTaylorSeriesUpToOn_succ_nat_iff_right
-- 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
m : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 f s x : (a : (i : Fin 0) → E) → F) m = f x

Tactic:
rfl

Premises used: 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
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)

Tactic:
rfl

Premises used: iteratedFDerivWithin, ContinuousMultilinearMap.constOfIsEmpty, ContinuousMultilinearMap.uncurry0, 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
f : E → F
s : Set E
x : E
g : E → F
t : Set E
y : E
⊢ dist (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s x)
      (iteratedFDerivWithin 𝕜 0 g t y) =
    dist (f x) (g y)

Tactic:
simp only [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.dist_map]

Premises used: LinearIsometryEquiv.dist_map, iteratedFDerivWithin_zero_eq_comp, Function.comp_apply
-- 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
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x) =
    ‖f x‖
rw₁ :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
          (f x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) =
    ‖f x‖
rw₂ rw₃ : ‖f x‖ = ‖f x‖
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s x) = ‖f x‖

Tactic:
rw [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, iteratedFDerivWithin_zero_eq_comp, Function.comp_apply
-- 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 : ℕ
m : Fin (n + 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)

Tactic:
rfl

Premises used: iteratedFDerivWithin, 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 : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s))

Tactic:
rfl

Premises used: ContinuousLinearMap.uncurryLeft, iteratedFDerivWithin, MultilinearMap.mkContinuous, 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
f : E → F
s : Set E
n : ℕ
⊢ Eq (α := (x : E) → E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s)
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) →
          E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s))

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, iteratedFDerivWithin, ContinuousMultilinearMap.curryLeft, MultilinearMap.mkContinuous, Fin.induction, MultilinearMap.mk', Fin.cases, MultilinearMap.mkContinuousLinear, Fin.tail, LinearMap.mkContinuous, rfl