awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
⊢ Eq.{uF + 1} (α := F)
    ((((ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
                  (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
                        F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
                    F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
                  ((continuousMultilinearCurryFin1 𝕜 E F :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                    (p x 1)) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
              y :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        v :
      F)
    ((((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0)) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
              y :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        v :
      F)
have h₁ : Eq.{uF + 1} (α := F) ((p x 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) 0 y) : F)
  ((p x 1 : (a : (i : Fin 1) → E) → F) (cons (α := fun (i : Fin 1) ↦ E) y v) : F)
Tactic: change (p x 1) (snoc 0 y) = (p x 1) (cons y v)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
⊢ Eq.{uF + 1} (α := F) ((p x 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) 0 y) : F)
    ((p x 1 : (a : (i : Fin 1) → E) → F) (cons (α := fun (i : Fin 1) ↦ E) y v) : F)
have h₁ : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
  Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y i : E) (cons (α := fun (i : Fin 1) ↦ E) y v i : E)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
A :
  ∀ y ∈ s,
    f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E))
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)) NormedSpace.toModule (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin 0) ↦ E))
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E))
y : E
v : (i : Fin 0) → E
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y i : E) (cons (α := fun (i : Fin 1) ↦ E) y v i : E)
have h₁ : Eq.{uE + 1} (α := E) (snoc (α := fun (i : Fin 1) ↦ E) 0 y default : E) (cons (α := fun (i : Fin 1) ↦ E) y v default : E)
Tactic: rw [Unique.eq_default (α := Fin 1) i]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 : ℕ
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s ↔
    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
have mp : HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s →
  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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 : ℕ
mp :
  HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s →
    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
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s ↔
    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
have mpr : 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 →
  HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s
have mpr : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
mpr : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s
have mpr₁ : ∀ (m : ℕ),
  (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 →
    ∀ 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: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
mpr : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
mpr₁ :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 →
      ∀ 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
⊢ HasFTaylorSeriesUpToOn (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f p s
have mpr₂ : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
⊢ ∀ 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
have pos : ∀ (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: by_cases h' : m < n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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),
    ∀ 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
⊢ ∀ 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
have neg : ∀ (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: by_cases h' : m < n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (hypothesis)
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
have this : m = n
Tactic: have : m = n := Nat.eq_of_lt_succ_of_not_lt (mod_cast hm) h'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 m) ↦ E) F) (fun (x : E) ↦ p x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
have 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
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
have pos : ∀ (h' : m ≤ n),
  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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
have neg : ∀ (h' : ¬m ≤ n),
  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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (hypothesis)
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
have this : m = n + 1
Tactic: have : m = n + 1 := le_antisymm (mod_cast hm) (not_le.1 h')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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 m) ↦ E) F) (fun (x : E) ↦ p x m) s
have neg : ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (fun (x : E) ↦ p x (n + 1))
  s
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
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
⊢ 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
have 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)
Tactic: constructor