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 : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : m < n
⊢ ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x

Tactic:
h.1.fderivWithin m (mod_cast h')

Premises used: Nat.cast_lt._simp_1, cast, HasFTaylorSeriesUpToOn.fderivWithin, And.left, Eq.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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : m < n
⊢ ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x

Tactic:
exact h.1.fderivWithin m (mod_cast h')

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

Tactic:
have : m = n := Nat.eq_of_lt_succ_of_not_lt (mod_cast hm) 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : ¬m < n
this : m = n
neg :
  ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (x : E) ↦ p x n)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x
⊢ ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x

Tactic:
rw [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 : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : ¬m < n
this : m = n
⊢ ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (x : E) ↦ p x n)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x

Tactic:
h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : ¬m < n
this : m = n
⊢ ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (x : E) ↦ p x n)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x

Tactic:
exact h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
pos :
  ∀ (h' : m ≤ n),
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
neg :
  ∀ (h' : ¬m ≤ n),
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s

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

Tactic:
apply h.1.cont m (mod_cast h')

Premises used: HasFTaylorSeriesUpToOn.cont, cast, Nat.cast_le._simp_1, And.left, Eq.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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : ¬m ≤ n
⊢ m = n + 1

Tactic:
have : m = n + 1 := le_antisymm (mod_cast hm) (not_le.1 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : ¬m ≤ n
this : m = n + 1
neg :
  ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (fun (x : E) ↦ p x (n + 1)) s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s

Tactic:
rw [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 : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p s ∧
    (∀ x ∈ s,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (y : E) ↦ p y n)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin n.succ) ↦ E) (p x n.succ)) s x) ∧
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (fun (x : E) ↦ p x (n + 1)) s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1
h' : ¬m ≤ n
this : m = n + 1
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (fun (x : E) ↦ p x (n + 1)) s

Tactic:
h.2.2

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

Tactic:
exact h.2.2

Premises used: And.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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
zero_eq :
  ∀ x ∈ s,
    Eq (α := E →L[𝕜] F) (ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E) ((p x).shift 0) : E →L[𝕜] F)
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
          (p x 1) :
        E →L[𝕜] F)
fderivWithin :
  ∀ (m : ℕ),
    LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω) →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
          (fun (x : E) ↦ (p x).shift m)
          (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
            ((p x).shift m.succ))
          s x
cont :
  ∀ (m : ℕ),
    LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω) →
      ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ (p x).shift m) s
⊢ 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:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
x : E
zero_eq :
  x ∈ s →
    Eq (α := E →L[𝕜] F) (ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E) ((p x).shift 0) : E →L[𝕜] F)
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
          (p x 1) :
        E →L[𝕜] F)
⊢ x ∈ s →
    Eq (α := E →L[𝕜] F) (ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E) ((p x).shift 0) : E →L[𝕜] F)
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
          (p x 1) :
        E →L[𝕜] F)

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
x : E
h : x ∈ s
⊢ Eq (α := E →L[𝕜] F) (ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E) ((p x).shift 0) : E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p x 1) :
      E →L[𝕜] F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
fderivWithin :
  ∀ (hm : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)),
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
        (fun (x : E) ↦ (p x).shift m)
        (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
          ((p x).shift m.succ))
        s x
⊢ LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω) →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
        (fun (x : E) ↦ (p x).shift m)
        (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
          ((p x).shift m.succ))
        s x

Tactic:
(hm : (m : ℕ∞ω) < 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
x : E
fderivWithin :
  ∀ (hx : x ∈ s),
    HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
      (fun (x : E) ↦ (p x).shift m)
      (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
        ((p x).shift m.succ))
      s x
⊢ x ∈ s →
    HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
      (fun (x : E) ↦ (p x).shift m)
      (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
        ((p x).shift m.succ))
      s x

Tactic:
(hx : x ∈ s)
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
x : E
hx : x ∈ s
rw : ∀ (hm : m < n) (x : E) (hx : x ∈ s), m.succ < n.succ
⊢ LT.lt (α := ℕ∞ω) (↑m.succ : ℕ∞ω) (↑n.succ : ℕ∞ω)

Tactic:
rw [Nat.cast_lt] at hm ⊢

Premises used: Nat.cast_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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
hm : m < n
x : E
hx : x ∈ s
⊢ m.succ < n.succ

Tactic:
Nat.succ_lt_succ hm

Premises used: Nat.succ_lt_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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
hm : m < n
x : E
hx : x ∈ s
⊢ m.succ < n.succ

Tactic:
exact Nat.succ_lt_succ hm

Premises used: Nat.succ_lt_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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
x : E
hx : x ∈ s
⊢ LT.lt (α := ℕ∞ω) (↑m.succ : ℕ∞ω) (↑n.succ : ℕ∞ω)

Tactic:
have A : (m.succ : ℕ∞ω) < n.succ := by
      rw [Nat.cast_lt] at hm ⊢
      exact Nat.succ_lt_succ hm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
x : E
hx : x ∈ s
A : LT.lt (α := ℕ∞ω) (↑m.succ : ℕ∞ω) (↑n.succ : ℕ∞ω)
fderivWithin :
  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 + 1)) ↦ E) (G := E →L[𝕜] F)
      (ContinuousMultilinearMap.curryRight (Ei := fun (i : Fin m.succ.succ) ↦ E) (p x m.succ.succ)))
    s x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F))
    (fun (x : E) ↦ (p x).shift m)
    (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F) ((p x).shift m.succ))
    s x

Tactic:
change HasFDerivWithinAt (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
      (p x m.succ.succ).curryRight.curryLeft s x

Premises used: Function.comp, HasFDerivWithinAt, ContinuousMultilinearMap.curryLeft, continuousMultilinearCurryRightEquiv', ContinuousMultilinearMap.curryRight, Nat.succ, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
m : ℕ
cont :
  ∀ (hm : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)),
    ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ (p x).shift m) s
⊢ LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω) →
    ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ (p x).shift m) s

Tactic:
(hm : (m : ℕ∞ω) ≤ n)