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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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 : E
hx : x ∈ s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
A : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
this :
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (⇑(continuousMultilinearCurryRightEquiv' 𝕜 m E F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
      fun (x : E) ↦ p x m.succ)
    (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F) ((p x).shift m.succ))
    s x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
    (fun (x : E) ↦ p x m.succ)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) ≃L[𝕜]
              ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) →L[𝕜]
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
        ((p x).shift m.succ)))
    s x

Tactic:
rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'
            (f' := ((p x).shift m.succ).curryLeft)] at this

Premises used: LinearIsometryEquiv.comp_hasFDerivWithinAt_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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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 : E
hx : x ∈ s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
A : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
this :
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
    (fun (x : E) ↦ p x m.succ)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) ≃L[𝕜]
              ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) →L[𝕜]
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
        ((p x).shift m.succ)))
    s x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
    (fun (x : E) ↦ p x m.succ)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) ≃L[𝕜]
              ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) →L[𝕜]
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
        ((p x).shift m.succ)))
    s x

Tactic:
this
-- 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 : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
mpr :
  ∀ (hm : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n.succ : ℕ∞ω)),
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
⊢ LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑(n + 1) : ℕ∞ω) →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s

Tactic:
(hm : (m : ℕ∞ω) ≤ n.succ)
-- 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 : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n.succ : ℕ∞ω)
mpr :
  ∀ (hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) (↑n.succ : ℕ∞ω)),
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
mpr₁ :
  ∀ (m : ℕ) (hm : LE.le (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)),
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F)
      (fun (x : E) ↦ p x (m + 1)) s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s

Tactic:
rcases m with - | m
-- 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 : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) (↑n.succ : ℕ∞ω)
⊢ DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s

Tactic:
have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
          (Hfderiv_zero x hx).differentiableWithinAt
-- 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 : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) (↑n.succ : ℕ∞ω)
this :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s

Tactic:
this.continuousOn

Premises used: DifferentiableOn.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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) (↑n.succ : ℕ∞ω)
this :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s

Tactic:
exact this.continuousOn

Premises used: DifferentiableOn.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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F)
    (fun (x : E) ↦ p x (m + 1)) s

Tactic:
(continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_

Premises used: continuousMultilinearCurryRightEquiv', Iff.mp, LinearIsometryEquiv.comp_continuousOn_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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
mpr :
  ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (⇑(continuousMultilinearCurryRightEquiv' 𝕜 m E F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
      fun (x : E) ↦ p x (m + 1))
    s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F)
    (fun (x : E) ↦ p x (m + 1)) s

Tactic:
refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_

Premises used: continuousMultilinearCurryRightEquiv', Iff.mp, LinearIsometryEquiv.comp_continuousOn_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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (⇑(continuousMultilinearCurryRightEquiv' 𝕜 m E F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
      fun (x : E) ↦ p x (m + 1))
    s

Tactic:
Htaylor.cont _ ?_

Premises used: HasFTaylorSeriesUpToOn.cont, MultilinearMap.mkContinuous, ContinuousMultilinearMap.curryRight, FormalMultilinearSeries.shift
-- 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 : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
mpr : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (⇑(continuousMultilinearCurryRightEquiv' 𝕜 m E F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
      fun (x : E) ↦ p x (m + 1))
    s

Tactic:
refine Htaylor.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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
mpr : ∀ (hm : m + 1 ≤ n.succ), m ≤ n
⊢ LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)

Tactic:
rw [Nat.cast_le] at hm ⊢

Premises used: Nat.cast_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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : m + 1 ≤ n.succ
⊢ m ≤ n

Tactic:
Nat.lt_succ_iff.mp hm

Premises used: Nat.lt_succ_iff, Iff.mp
-- 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 : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ 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
Htaylor :
  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
m : ℕ
hm : m + 1 ≤ n.succ
⊢ m ≤ n

Tactic:
exact Nat.lt_succ_iff.mp hm

Premises used: Nat.lt_succ_iff, Iff.mp
-- 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
⊢ HasFTaylorSeriesUpToOn N 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:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.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
refine_1 :
  ∀ (h : HasFTaylorSeriesUpToOn N 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
refine_2 :
  ∀
    (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),
    HasFTaylorSeriesUpToOn N f p s
⊢ HasFTaylorSeriesUpToOn N 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:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : HasFTaylorSeriesUpToOn N f p s
⊢ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s

Tactic:
rw [hasFTaylorSeriesUpToOn_top_iff_add hN 1] at h

Premises used: OfNat.ofNat, hasFTaylorSeriesUpToOn_top_iff_add