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 : ℕ
a : E
zero :
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 0 f (a +ᵥ s) (a + x)
succ :
  ∀ (n : ℕ)
    (IH :
      Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦
        iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)),
    Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦
      iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + x)
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

Tactic:
induction n with
  | zero => simp [iteratedFDerivWithin]
  | succ n IH =>
    ext v
    simp [iteratedFDerivWithin_succ_eq_comp_left, IH, fderivWithin_comp_add_left]

Premises used: fderivWithin_comp_add_left, iteratedFDerivWithin_succ_eq_comp_left, Fin.succ, iteratedFDerivWithin
-- 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 : ℕ
a x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s x) (iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x))

Tactic:
simp [iteratedFDerivWithin_comp_add_left']

Premises used: iteratedFDerivWithin_comp_add_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
n : ℕ
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (z + a)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

Tactic:
simpa [add_comm a] using iteratedFDerivWithin_comp_add_left' n a

Premises used: add_comm, iteratedFDerivWithin_comp_add_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
n : ℕ
a x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (z + a)) s x) (iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a))

Tactic:
simp [iteratedFDerivWithin_comp_add_right']

Premises used: iteratedFDerivWithin_comp_add_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 : ℕ
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (z - a)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Tactic:
simpa [sub_eq_add_neg] using iteratedFDerivWithin_comp_add_right' n (-a)

Premises used: iteratedFDerivWithin_comp_add_right', sub_eq_add_neg, Neg.neg
-- 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 : ℕ
a : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (z - a)) s x) (iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a))

Tactic:
simp [iteratedFDerivWithin_comp_sub']

Premises used: iteratedFDerivWithin_comp_sub'
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
rw :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (ContinuousMultilinearMap.curry0 (p x 0)))
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (f x))

Tactic:
rw [← h.zero_eq x]

Premises used: HasFTaylorSeriesUpTo.zero_eq
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (ContinuousMultilinearMap.curry0 (p x 0)))

Tactic:
(p x 0).uncurry0_curry0.symm

Premises used: ContinuousMultilinearMap.constOfIsEmpty, ContinuousMultilinearMap.uncurry0, OfNat.ofNat, Eq.symm, ContinuousMultilinearMap.uncurry0_curry0
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (ContinuousMultilinearMap.curry0 (p x 0)))

Tactic:
exact (p x 0).uncurry0_curry0.symm

Premises used: OfNat.ofNat, Eq.symm, ContinuousMultilinearMap.uncurry0_curry0
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : (↑m : ℕ∞ω) < n
x : E
⊢ Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fderiv 𝕜 (fun (x : E) ↦ p x m) x)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))

Tactic:
h.fderiv m hmn x |>.fderiv

Premises used: HasFDerivAt.fderiv, HasFTaylorSeriesUpTo.fderiv
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
mp : HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p
mpr : HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ
⊢ HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p

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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (x : E), ContinuousMultilinearMap.curry0 (p x 0) = f x

Tactic:
simpa using H.zero_eq

Premises used: HasFTaylorSeriesUpToOn.zero_eq
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), (↑m : ℕ∞ω) ≤ n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ p x m

Tactic:
simpa using H.cont

Premises used: HasFTaylorSeriesUpToOn.cont
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
mp :
  ∀ (H : HasFTaylorSeriesUpToOn n f p univ) (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : E),
        HasFDerivAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (y : E) ↦ p y m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) x
⊢ HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p

Tactic:
refine fun H ↦ ⟨by simpa using H.zero_eq, ?_, by simpa using H.cont⟩
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (x : E), Membership.mem (γ := Set E) univ x → ContinuousMultilinearMap.curry0 (p x 0) = f x

Tactic:
simpa using H.zero_eq

Premises used: HasFTaylorSeriesUpTo.zero_eq
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) univ

Tactic:
simpa using H.cont

Premises used: HasFTaylorSeriesUpTo.cont
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
mpr :
  ∀ (H : HasFTaylorSeriesUpTo n f p) (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : E),
        Membership.mem (γ := Set E) univ x →
          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))
            univ x
⊢ HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ

Tactic:
refine fun H ↦ ⟨by simpa using H.zero_eq, ?_, by simpa using H.cont⟩
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : E),
        HasFDerivAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (y : E) ↦ p y m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) x

Tactic:
simpa using H.fderivWithin

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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : E),
        Membership.mem (γ := Set E) univ x →
          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))
            univ x

Tactic:
simpa using H.fderiv

Premises used: HasFTaylorSeriesUpTo.fderiv
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
s : Set E
⊢ HasFTaylorSeriesUpToOn n f p s

Tactic:
(hasFTaylorSeriesUpToOn_univ_iff.2 h).mono (subset_univ _)

Premises used: Iff.mpr, hasFTaylorSeriesUpToOn_univ_iff, Set.subset_univ, HasFTaylorSeriesUpToOn.mono
-- 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
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hmn : m ≤ n
rw : ∀ (h : HasFTaylorSeriesUpToOn n f p univ) (hmn : m ≤ n), HasFTaylorSeriesUpToOn m f p univ
⊢ HasFTaylorSeriesUpTo m f p

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h ⊢

Premises used: hasFTaylorSeriesUpToOn_univ_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
f : E → F
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
hmn : m ≤ n
⊢ HasFTaylorSeriesUpToOn m f p univ

Tactic:
h.of_le hmn

Premises used: HasFTaylorSeriesUpToOn.of_le
-- 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
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
hmn : m ≤ n
⊢ HasFTaylorSeriesUpToOn m f p univ

Tactic:
exact h.of_le hmn

Premises used: HasFTaylorSeriesUpToOn.of_le
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
⊢ HasFTaylorSeriesUpToOn n f p univ

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h

Premises used: hasFTaylorSeriesUpToOn_univ_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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
rw : ContinuousOn f univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ ContinuousOn f univ

Tactic:
h.continuousOn

Premises used: HasFTaylorSeriesUpToOn.continuousOn
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ ContinuousOn f univ

Tactic:
exact h.continuousOn

Premises used: HasFTaylorSeriesUpToOn.continuousOn
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpTo 0 f p ↔
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        f ∧
      ∀ (x : E), ContinuousMultilinearMap.curry0 (p x 0) = f x

Tactic:
simp [hasFTaylorSeriesUpToOn_univ_iff.symm, continuousOn_univ,
    hasFTaylorSeriesUpToOn_zero_iff]

Premises used: hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_zero_iff, continuousOn_univ, Iff.symm
-- 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpTo N f p ↔ ∀ (n : ℕ), HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f p

Tactic:
simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff hN]

Premises used: hasFTaylorSeriesUpToOn_univ_iff, 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
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpTo N f p ↔
    (∀ (x : E), ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      ∀ (m : ℕ) (x : E),
        HasFDerivAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (y : E) ↦ p y m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) x

Tactic:
simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff' hN, mem_univ,
    forall_true_left, hasFDerivWithinAt_univ]

Premises used: forall_true_left, hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff', Set.mem_univ, hasFDerivWithinAt_univ
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
x : E
rw :
  HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    univ 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:
rw [← hasFDerivWithinAt_univ]

Premises used: hasFDerivWithinAt_univ
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
x : E
⊢ HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    univ x

Tactic:
(hasFTaylorSeriesUpToOn_univ_iff.2 h).hasFDerivWithinAt hn (mem_univ _)

Premises used: Iff.mpr, hasFTaylorSeriesUpToOn_univ_iff, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, Set.mem_univ
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
x : E
⊢ HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    univ x

Tactic:
exact (hasFTaylorSeriesUpToOn_univ_iff.2 h).hasFDerivWithinAt hn (mem_univ _)

Premises used: Iff.mpr, hasFTaylorSeriesUpToOn_univ_iff, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, Set.mem_univ
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
⊢ Differentiable 𝕜 f

Tactic:
fun x => (h.hasFDerivAt hn x).differentiableAt

Premises used: Differentiable, HasFTaylorSeriesUpTo.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
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpTo (↑(n + 1) : ℕ∞ω) f p ↔
    (∀ (x : E), ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
      (∀ (x : E),
          HasFDerivAt (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)) x) ∧
        HasFTaylorSeriesUpTo (𝕜 := 𝕜) (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

Tactic:
simp only [hasFTaylorSeriesUpToOn_succ_nat_iff_right, ← hasFTaylorSeriesUpToOn_univ_iff, mem_univ,
    forall_true_left, hasFDerivWithinAt_univ]

Premises used: forall_true_left, hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_succ_nat_iff_right, Set.mem_univ, hasFDerivWithinAt_univ
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
h2 : (↑k : ℕ∞ω) ≤ n
⊢ Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)

Tactic:
rfl