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
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 : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
have 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
Tactic: rcases m with - | m
Cleared hypotheses: m, hm
-- 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 : ℕ
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
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
have 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
Tactic: rcases m with - | m
Cleared hypotheses: m, hm
-- 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 : ℕ
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 : ℕ∞ω)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
have this : 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
-- 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 : ℕ
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
have 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
Tactic: refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_
-- 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 : ℕ
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
have mpr : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
Tactic: refine Htaylor.cont _ ?_
-- 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 : ℕ
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 : ℕ∞ω)
⊢ LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
have mpr : ∀ (hm : m + 1 ≤ n.succ), m ≤ n
Tactic: rw [Nat.cast_le] at hm ⊢
Cleared hypotheses: hm
-- 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
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun 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
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
⊢ 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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
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
have h₁ : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
Tactic: rw [hasFTaylorSeriesUpToOn_top_iff_add hN 1] at h
Cleared hypotheses: 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) 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
have refine_1 : (∀ 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) ∧
    ∀ (n : ℕ),
      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: rw [hasFTaylorSeriesUpToOn_top_iff hN]
-- 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
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
have apply : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
Tactic: apply (hasFTaylorSeriesUpToOn_top_iff_add hN 1).2 (fun 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
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
n : ℕ
⊢ HasFTaylorSeriesUpToOn (↑(n + 1) : ℕ∞ω) f p s
have rw : (∀ 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: rw [hasFTaylorSeriesUpToOn_succ_nat_iff_right]
-- 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
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s x) = ‖f x‖
have rw : norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
        f)
      x) =
  ‖f x‖
Tactic: rw [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
-- 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
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x) =
    ‖f x‖
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s x) = ‖f x‖
have rw₁ : norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) =
  ‖f x‖
Tactic: rw [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
-- 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
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x) =
    ‖f x‖
rw₁ :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
          (f x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) =
    ‖f x‖
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s x) = ‖f x‖
have rw₂ : ‖f x‖ = ‖f x‖
Tactic: rw [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
-- 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 : ℕ
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)
have rw : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]
-- 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 : ℕ
rw :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x)
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)
have rw₁ : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]