awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
y : E
hy : y ∈ v ∩ u
z : E
⊢ Eq.{uF + 1} (α := F)
    (((↑(↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F))) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F ≃L[𝕜] F) :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F →L[𝕜] F) ∘SL
            ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1) :
          (a : E) → F)
        z :
      F)
    ((ContinuousMultilinearMap.curry0 (p' y 0) : (a : E) → F) z : F)
have h : Eq.{uF + 1} (α := F)
  ((((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
            (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
              (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0)) :
          E →L[𝕜] F) :
        (a : E) → F)
      (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0 (last 0) : E) :
    F)
  (((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) z : F)
Tactic: change ((p' y 0) (init (@cons 0 (fun _ => E) z 0))) (@cons 0 (fun _ => E) z 0 (last 0)) =
          ((p' y 0) 0) z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
y : E
hy : y ∈ v ∩ u
z : E
⊢ Eq.{uF + 1} (α := F)
    ((((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0 (last 0) : E) :
      F)
    (((p' y 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) z : F)
have h : Eq.{uE + 1} (α := (i : Fin 0) → E)
  (init (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) (cons (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) z 0) :
    (i : Fin 0) → E)
  (0 : (i : Fin 0) → E)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ 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).unshift (f x) 1))
    (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
have h : Eq (α := E → E →L[𝕜] F)
  (fun (x : E) ↦
    (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      ((p' x).unshift (f x) 1))
  fun (x : E) ↦ ContinuousMultilinearMap.curry0 (p' x 0)
Tactic: convert! (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
h :
  Eq (α := E → E →L[𝕜] F)
    (fun (x : E) ↦
      (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((p' x).unshift (f x) 1))
    fun (x : E) ↦ ContinuousMultilinearMap.curry0 (p' x 0)
⊢ 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).unshift (f x) 1))
    (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
have h₁ : (fun (x : E) ↦ ((p' x).unshift (f x)).shift) = p'
Tactic: convert! (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ Eq (α := E → E →L[𝕜] F)
    (fun (x : E) ↦
      (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((p' x).unshift (f x) 1))
    fun (x : E) ↦ ContinuousMultilinearMap.curry0 (p' x 0)
have h : ∀ (x y : E),
  Eq.{uF + 1} (α := F)
    ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
              ((p' x).unshift (f x) 1) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    ((ContinuousMultilinearMap.curry0 (p' x 0) : (a : E) → F) y : F)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x_1
v : Set E
hv : v ∈ 𝓝[insert x_1 u] x_1
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
x y : E
⊢ Eq.{uF + 1} (α := F)
    ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
              ((p' x).unshift (f x) 1) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    ((ContinuousMultilinearMap.curry0 (p' x 0) : (a : E) → F) y : F)
have h : Eq.{uF + 1} (α := F)
  ((((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
            (init (α := fun (x : Fin 1) ↦ E) (snoc (α := fun (x : Fin 1) ↦ E) 0 y)) :
          E →L[𝕜] F) :
        (a : E) → F)
      y :
    F)
  (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
Tactic: change p' x 0 (init (@snoc 0 (fun _ : Fin 1 => E) 0 y)) y = p' x 0 0 y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x_1
v : Set E
hv : v ∈ 𝓝[insert x_1 u] x_1
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
x y : E
⊢ Eq.{uF + 1} (α := F)
    ((((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin 1) ↦ E) (snoc (α := fun (x : Fin 1) ↦ E) 0 y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
have h : Eq.{uF + 1} (α := F) (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
  (((p' x 0 : (a : (i : Fin 0) → E) → E →L[𝕜] F) 0 : (a : E) → F) y : F)
Tactic: rw [init_snoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
⊢ (fun (x : E) ↦ ((p' x).unshift (f x)).shift) = p'
have h : ∀ (x : E) (k : ℕ) (v : (i : Fin k) → E) (y : E),
  Eq.{uF + 1} (α := F)
    ((((((p' x).unshift (f x)).shift k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
Tactic: ext x k v y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x_1
v_1 : Set E
hv : v_1 ∈ 𝓝[insert x_1 u] x_1
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v_1
p'_an :
  n = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v_1
x : E
k : ℕ
v : (i : Fin k) → E
y : E
⊢ Eq.{uF + 1} (α := F)
    ((((((p' x).unshift (f x)).shift k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
have h : Eq.{uF + 1} (α := F)
  ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F)
            (init (α := fun (x : Fin k.succ) ↦ E) (snoc (α := fun (x : Fin k.succ) ↦ E) v y)) :
          E →L[𝕜] F) :
        (a : E) → F)
      (snoc (α := fun (x : Fin k.succ) ↦ E) v y (last k) : E) :
    F)
  ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
Tactic: change p' x k (init (@snoc k (fun _ : Fin k.succ => E) v y))
            (@snoc k (fun _ : Fin k.succ => E) v y (last k)) = p' x k v y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x_1
v_1 : Set E
hv : v_1 ∈ 𝓝[insert x_1 u] x_1
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v_1
p'_an :
  n = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v_1
x : E
k : ℕ
v : (i : Fin k) → E
y : E
⊢ Eq.{uF + 1} (α := F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin k.succ) ↦ E) (snoc (α := fun (x : Fin k.succ) ↦ E) v y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (snoc (α := fun (x : Fin k.succ) ↦ E) v y (last k) : E) :
      F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
have h : Eq.{uF + 1} (α := F)
  ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F)
            (init (α := fun (x : Fin k.succ) ↦ E) (snoc (α := fun (x : Fin k.succ) ↦ E) v y)) :
          E →L[𝕜] F) :
        (a : E) → F)
      y :
    F)
  ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
Tactic: rw [snoc_last, init_snoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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_1 : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x_1 s] x_1
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x_1
v_1 : Set E
hv : v_1 ∈ 𝓝[insert x_1 u] x_1
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v_1
p'_an :
  n = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v_1
x : E
k : ℕ
v : (i : Fin k) → E
y : E
h :
  Eq.{uF + 1} (α := F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin k.succ) ↦ E) (snoc (α := fun (x : Fin k.succ) ↦ E) v y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
⊢ Eq.{uF + 1} (α := F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F)
              (init (α := fun (x : Fin k.succ) ↦ E) (snoc (α := fun (x : Fin k.succ) ↦ E) v y)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (snoc (α := fun (x : Fin k.succ) ↦ E) v y (last k) : E) :
      F)
    ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
have h₁ : Eq.{uF + 1} (α := F) ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
  ((((p' x k : (a : (i : Fin k) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) y : F)
Tactic: rw [snoc_last, init_snoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
h : n + 1 = ω
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ (fun (x : E) ↦ (p' x).unshift (f x)) x i) (v ∩ u)
have h₁ : n = ω
Tactic: simp only [WithTop.add_eq_top, WithTop.one_ne_top, or_false] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
i : ℕ
h : n = ω
⊢ AnalyticOn 𝕜 (F := 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))
    (v ∩ u)
have apply : AnalyticOnNhd 𝕜 (E := F) (F := 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)
  univ
Tactic: apply AnalyticOnNhd.comp_analyticOn _ ((hf h).mono inter_subset_right)
          (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an :
  n = ω →
    ∀ (i : ℕ), AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (fun (x : E) ↦ p' x i) v
i_1 : ℕ
h : n = ω
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (fun (x : E) ↦
      (LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 i E F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
        (p' x i))
    (v ∩ u)
have apply : AnalyticOnNhd 𝕜 (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) (F :=
  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
  (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 i E F)) :
    (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F)) →
      ContinuousMultilinearMap 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
  univ
Tactic: apply AnalyticOnNhd.comp_analyticOn _ ((p'_an h i).mono inter_subset_left)
          (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_1 : ∀ (hf : ContDiffWithinAt 𝕜 (n + 1) f s x),
  ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
Tactic: refine ⟨fun hf => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
refine_1 :
  ∀ (hf : ContDiffWithinAt 𝕜 (n + 1) f s x),
    ∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_2 : (∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
  ContDiffWithinAt 𝕜 (n + 1) f s x
Tactic: refine ⟨fun hf => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_1 : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (f_an : n = ω → AnalyticOn 𝕜 f u) (f' : E → E →L[𝕜] F)
  (huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) (hf' : ContDiffWithinAt 𝕜 n f' u x),
  ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
Tactic: obtain ⟨u, hu, f_an, f', huf', hf'⟩ := (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).mp hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_1 : ∀ (w : Set E) (hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w) (hxw : x ∈ w)
  (hwu : w ∩ insert x s ⊆ u),
  ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
Tactic: obtain ⟨w, hw, hxw, hwu⟩ := mem_nhdsWithin.mp hu