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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
⊢ HasFTaylorSeriesUpToOn n f₁ p s
have refine : ∀ (x : E) (hx : x ∈ s), ContinuousMultilinearMap.curry0 (p x 0) = f₁ x
Tactic: refine ⟨fun x hx => ?_, h.fderivWithin, h.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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ ContinuousMultilinearMap.curry0 (p x 0) = f₁ x
have rw : ContinuousMultilinearMap.curry0 (p x 0) = f x
Tactic: rw [h₁ x hx]
-- 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ q x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ)) s x
have refine : Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
  (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))
  (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ))
Tactic: refine ((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_
-- 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 q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
        (fun (x : E) ↦ q x m) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ))
have refine : (↑(m + 1) : ℕ∞ω) ≤ n
Tactic: refine congrArg _ (hpq (m + 1) ?_ hx)
-- 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
h : HasFTaylorSeriesUpToOn n f p s
⊢ ContinuousOn f s
have this : ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
  (fun (x : E) ↦
    (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (f x))
  s
Tactic: have := (h.cont 0 bot_le).congr fun x hx => (h.zero_eq' hx).symm
-- 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
h : HasFTaylorSeriesUpToOn n f p s
this :
  ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (x : E) ↦
      (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x))
    s
⊢ ContinuousOn f s
have rwa : ContinuousOn (Y := 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)
  s
Tactic: rwa [← (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_continuousOn_iff]
-- 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
⊢ HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
have refine : ∀ (H : ContinuousOn f s ∧ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x) (m : ℕ)
  (hm : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) 0),
  ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
Tactic: refine ⟨fun H => ⟨H.continuousOn, H.zero_eq⟩, fun H =>
      ⟨H.2, fun m hm => False.elim (not_le.2 hm bot_le), fun 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
H : ContinuousOn f s ∧ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
m : ℕ
hm : LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) 0
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) s
have obtain : ∀ (hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) 0),
  ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
Tactic: obtain rfl : m = 0 := mod_cast hm.antisymm zero_le
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
H : ContinuousOn f s ∧ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) 0
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
have this : EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0)
  ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
      (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
    f)
  s
Tactic: have : EqOn (p · 0) ((continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s := fun x hx ↦
    (continuousMultilinearCurryFin0 𝕜 E F).eq_symm_apply.2 (H.2 x hx)
-- 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
H : ContinuousOn f s ∧ ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
hm : LE.le (α := ℕ∞ω) (↑0 : ℕ∞ω) 0
this :
  EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)
    s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
have rw : ContinuousOn f s
Tactic: rw [continuousOn_congr this, LinearIsometryEquiv.comp_continuousOn_iff]
-- 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
k : ℕ
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
have mp : HasFTaylorSeriesUpToOn N f p s → ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
mp : HasFTaylorSeriesUpToOn N f p s → ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
have mpr : (∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s) → HasFTaylorSeriesUpToOn N 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
⊢ HasFTaylorSeriesUpToOn N 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
mpr : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
⊢ HasFTaylorSeriesUpToOn N f p s
have mpr₁ : ∀ (m : ℕ),
  (↑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: 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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
mpr : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
mpr₁ :
  ∀ (m : ℕ),
    (↑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
⊢ HasFTaylorSeriesUpToOn N f p s
have mpr₂ : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ N →
    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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k) : ℕ∞ω) f p s
m : ℕ
h : (↑m : ℕ∞ω) < N
⊢ LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑(m.succ + k) : ℕ∞ω)
have norm_cast : m < m.succ + k
Tactic: norm_cast
-- 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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hn : n ≠ 0
hx : x ∈ s
⊢ HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    s x
have A : ∀ y ∈ s,
  f y = (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p y 0)
Tactic: have A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0) := fun y hy ↦
    (h.zero_eq y hy).symm
-- 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)
⊢ HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    s x
have suffices : HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) (F := F)
  (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (⇑(continuousMultilinearCurryFin0 𝕜 E F) : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F)
    fun (x : E) ↦ p x 0)
  ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
    (p x 1))
  s x
Tactic: suffices H : HasFDerivWithinAt (continuousMultilinearCurryFin0 𝕜 E F ∘ (p · 0))
    (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x from H.congr A (A x hx)
-- 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)
⊢ HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) (F := F)
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (⇑(continuousMultilinearCurryFin0 𝕜 E F) : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F)
      fun (x : E) ↦ p x 0)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    s x
have rw : HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
  (fun (x : E) ↦ p x 0)
  (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)))
  s x
Tactic: rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
-- 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
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)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (x : E) ↦ p x 0)
    (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)))
    s x
have this : (↑(↑0 : ℕ∞) : ℕ∞ω) < n
Tactic: have : ((0 : ℕ) : ℕ∞) < n := pos_iff_ne_zero.mpr 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
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
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (x : E) ↦ p x 0)
    (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)))
    s x
have h₁ : Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
    NormedAddCommGroup.toAddCommGroup (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin 0) ↦ E)) →
  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)) →
    Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F))
        UniformSpace.toTopologicalSpace (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin 0) ↦ E)) →
      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)) =
        ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0))
Tactic: convert! h.fderivWithin _ this x hx
-- 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))
⊢ 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)) =
    ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (Nat.succ 0)) ↦ E) (p x (Nat.succ 0))
have h₁ : ∀ (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)
Tactic: ext y v