awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s

Tactic:
((contDiffOn_succ_iff_derivWithin hs).1 (h.of_le hn)).2.2.continuousOn

Premises used: ContDiffOn.of_le, And.right, ContDiffOn.continuousOn, Iff.mp, contDiffOn_succ_iff_derivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s

Tactic:
exact ((contDiffOn_succ_iff_derivWithin hs).1 (h.of_le hn)).2.2.continuousOn

Premises used: ContDiffOn.of_le, And.right, ContDiffOn.continuousOn, Iff.mp, contDiffOn_succ_iff_derivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 1 ≤ n
⊢ HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
⊢ ContinuousOn (deriv f) s

Tactic:
((contDiffOn_succ_iff_deriv_of_isOpen hs).1 (h.of_le hn)).2.2.continuousOn

Premises used: contDiffOn_succ_iff_deriv_of_isOpen, ContDiffOn.of_le, And.right, ContDiffOn.continuousOn, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
⊢ ContinuousOn (deriv f) s

Tactic:
exact ((contDiffOn_succ_iff_deriv_of_isOpen hs).1 (h.of_le hn)).2.2.continuousOn

Premises used: contDiffOn_succ_iff_deriv_of_isOpen, ContDiffOn.of_le, And.right, ContDiffOn.continuousOn, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
H : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := F) m (fun (f : 𝕜 →L[𝕜] F) ↦ (f : (a : 𝕜) → F) 1) univ (fderivWithin 𝕜 f s x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
H : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 m (derivWithin f s) s x

Tactic:
exact ContDiffWithinAt.comp _ (by fun_prop) (g := fun f ↦ f 1) (t := .univ)
    (H.fderivWithin_right hs hmn hx) (fun _ _ ↦ trivial)

Premises used: trivial, ContDiffWithinAt.comp, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
⊢ ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 n (deriv f)

Tactic:
simp only [← contDiffOn_univ, contDiffOn_succ_iff_deriv_of_isOpen, isOpen_univ,
    differentiableOn_univ]

Premises used: differentiableOn_univ, contDiffOn_succ_iff_deriv_of_isOpen, isOpen_univ, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
rw :
  Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 0 (deriv f) ↔
    Differentiable 𝕜 f ∧ Continuous (deriv f)
⊢ ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (deriv f)

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl, contDiff_succ_iff_deriv]

Premises used: contDiff_succ_iff_deriv, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 0 (deriv f) ↔
    Differentiable 𝕜 f ∧ Continuous (deriv f)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
rw :
  Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (deriv f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (deriv f)
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (deriv f)

Tactic:
rw [show (∞ : ℕ∞ω) = ∞ + 1 from rfl, contDiff_succ_iff_deriv]

Premises used: contDiff_succ_iff_deriv, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (deriv f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (deriv f)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 1 ≤ n
⊢ HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
⊢ Continuous (deriv f)

Tactic:
(contDiff_succ_iff_deriv.mp (h.of_le hn)).2.2.continuous

Premises used: ContDiff.continuous, ContDiff.of_le, And.right, Iff.mp, contDiff_succ_iff_deriv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
⊢ Continuous (deriv f)

Tactic:
exact (contDiff_succ_iff_deriv.mp (h.of_le hn)).2.2.continuous

Premises used: ContDiff.continuous, ContDiff.of_le, And.right, Iff.mp, contDiff_succ_iff_deriv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ContDiff 𝕜 1 f
⊢ Continuous (deriv f)

Tactic:
ContDiff.continuous_deriv h (le_refl 1)

Premises used: le_refl, ContDiff.continuous_deriv, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ContDiff 𝕜 2 f
unfold : Differentiable.{u_1, u_1, u_2} 𝕜 (F := F) fun (x : 𝕜) ↦ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1
⊢ Differentiable 𝕜 (deriv f)

Tactic:
unfold deriv

Premises used: deriv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ContDiff 𝕜 2 f
⊢ Differentiable.{u_1, u_1, u_2} 𝕜 (F := F) fun (x : 𝕜) ↦ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : 𝕜 → F
x : 𝕜
H : ContDiffAt 𝕜 n f x
hmn : m + 1 ≤ n
⊢ UniqueDiffOn 𝕜 (E := 𝕜) univ

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : 𝕜 → F
x : 𝕜
H : ContDiffAt 𝕜 n f x
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (deriv f) x

Tactic:
simpa using ContDiffWithinAt.derivWithin (s := .univ) H.contDiffWithinAt (by simp) hmn

Premises used: ContDiffWithinAt.derivWithin, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 (n + 1) f
unfold : ContDiff.{u_1, u_1, u_2} 𝕜 (F := F) n fun (x : 𝕜) ↦ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1
⊢ ContDiff 𝕜 n (deriv f)

Tactic:
unfold deriv

Premises used: deriv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 (n + 1) f
⊢ ContDiff.{u_1, u_1, u_2} 𝕜 (F := F) n fun (x : 𝕜) ↦ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1

Tactic:
fun_prop
-- 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
x : E
hx : x ∈ s
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 hx]

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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
x : E
hx : x ∈ s
⊢ 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
x : E
hx : x ∈ s
⊢ 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
zero_eq : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → ContinuousMultilinearMap.curry0 (p x 0) = f x
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : E),
        Membership.mem (γ := Set E) ∅ 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)) ∅ x
cont :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) ∅
⊢ HasFTaylorSeriesUpToOn 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
⊢ ∀ (x : E), Membership.mem (γ := Set E) ∅ x → ContinuousMultilinearMap.curry0 (p x 0) = f x

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

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

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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
⊢ HasFTaylorSeriesUpToOn n f₁ p s

Tactic:
⟨fun x hx => ?_, h.fderivWithin, h.cont⟩

Premises used: HasFTaylorSeriesUpToOn.cont, HasFTaylorSeriesUpToOn.fderivWithin, HasFTaylorSeriesUpToOn.mk
-- 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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
refine : ∀ (x : E) (hx : x ∈ s), ContinuousMultilinearMap.curry0 (p x 0) = f₁ x
⊢ HasFTaylorSeriesUpToOn n f₁ p s

Tactic:
refine ⟨fun x hx => ?_, h.fderivWithin, 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
s : Set E
f f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
rw : ContinuousMultilinearMap.curry0 (p x 0) = f x
⊢ ContinuousMultilinearMap.curry0 (p x 0) = f₁ x

Tactic:
rw [h₁ x hx]
-- 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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ ContinuousMultilinearMap.curry0 (p x 0) = f x

Tactic:
h.zero_eq x hx

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

Tactic:
exact h.zero_eq x hx

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
s : Set E
f : E → F
n : ℕ∞ω
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
x : E
hx : x ∈ s
⊢ ContinuousMultilinearMap.curry0 (q x 0) = f x

Tactic:
simp only [← hpq 0 zero_le hx, hp.zero_eq x hx]

Premises used: zero_le, HasFTaylorSeriesUpToOn.zero_eq, 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ q x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ)) s x

Tactic:
((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_

Premises used: HasFDerivWithinAt.congr_fderiv, LT.lt.le, HasFTaylorSeriesUpToOn.fderivWithin, Set.EqOn.symm, HasFDerivWithinAt.congr'
-- 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
refine :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ))
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ q x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ)) s x

Tactic:
refine ((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_

Premises used: HasFDerivWithinAt.congr_fderiv, LT.lt.le, HasFTaylorSeriesUpToOn.fderivWithin, Set.EqOn.symm, HasFDerivWithinAt.congr'
-- 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ))

Tactic:
congrArg _ (hpq (m + 1) ?_ hx)

Premises used: congrArg, HAdd.hAdd, 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
refine : (↑(m + 1) : ℕ∞ω) ≤ n
⊢ Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ))

Tactic:
refine congrArg _ (hpq (m + 1) ?_ hx)

Premises used: congrArg, HAdd.hAdd, 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ (↑(m + 1) : ℕ∞ω) ≤ n

Tactic:
ENat.add_one_natCast_le_withTop_of_lt hm

Premises used: ENat.add_one_natCast_le_withTop_of_lt
-- 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ (↑(m + 1) : ℕ∞ω) ≤ n

Tactic:
exact ENat.add_one_natCast_le_withTop_of_lt hm

Premises used: ENat.add_one_natCast_le_withTop_of_lt
-- 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
t : Set E
hst : t ⊆ s
⊢ HasFTaylorSeriesUpToOn n f p t

Tactic:
⟨fun x hx => h.zero_eq x (hst hx), fun m hm x hx => (h.fderivWithin m hm x (hst hx)).mono hst,
    fun m hm => (h.cont m hm).mono hst⟩

Premises used: HasFTaylorSeriesUpToOn.zero_eq, HasFTaylorSeriesUpToOn.cont, HasFTaylorSeriesUpToOn.fderivWithin, ContinuousOn.mono, HasFDerivWithinAt.mono, HasFTaylorSeriesUpToOn.mk