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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : Ne (α := ℕ∞ω) ω ∞
h'n : HAdd.hAdd (α := ℕ∞ω) ω 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s x
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        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)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) ω
        (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) u
H'p :
  HAdd.hAdd (α := ℕ∞ω) ω 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
    (fun (x : E) ↦ (fun (y : E) ↦ (p y).shift) x i) u
have mp : AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
  (fun (x : E) ↦
    (continuousMultilinearCurryRightEquiv' 𝕜 i E F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i.succ) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
      (p x (i + 1)))
  u
Tactic: change AnalyticOn 𝕜
        (fun x ↦ (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : Ne (α := ℕ∞ω) ω ∞
h'n : HAdd.hAdd (α := ℕ∞ω) ω 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s x
Hp :
  (∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x) ∧
    (∀ x ∈ u,
        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)) u x) ∧
      HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) ω
        (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) u
H'p :
  HAdd.hAdd (α := ℕ∞ω) ω 1 = ω →
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
    (fun (x : E) ↦
      (continuousMultilinearCurryRightEquiv' 𝕜 i E F :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin i.succ) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (E →L[𝕜] F))
        (p x (i + 1)))
    u
have apply : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i.succ) ↦ E) F) (fun (x : E) ↦ p x (i + 1)) u
Tactic: apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn
        ?_ (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
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x
have mpr : ∃ u ∈ 𝓝[insert x s] x,
  ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
    HasFTaylorSeriesUpToOn (n + 1) f p u ∧
      (n + 1 = ω →
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u)
Tactic: rw [contDiffWithinAt_iff_of_ne_infty h'n]
-- 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
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)
have mpr : ∀ (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),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)
Tactic: rcases (contDiffWithinAt_iff_of_ne_infty hn).1 Hf' with ⟨v, hv, p', Hp', p'_an⟩
-- 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
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)
have mpr : v ∩ u ∈ 𝓝[insert x s] x
Tactic: refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩
-- 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
mpr : v ∩ u ∈ 𝓝[insert x s] x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)
have mpr₁ : HasFTaylorSeriesUpToOn.{u, uE, uF} (𝕜 := 𝕜) (n + 1) f (fun (x : E) ↦ (p' x).unshift (f x)) (v ∩ u)
Tactic: refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩
-- 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
mpr : v ∩ u ∈ 𝓝[insert x s] x
mpr₁ : HasFTaylorSeriesUpToOn.{u, uE, uF} (𝕜 := 𝕜) (n + 1) f (fun (x : E) ↦ (p' x).unshift (f x)) (v ∩ u)
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn (n + 1) f p u ∧
        (n + 1 = ω →
          ∀ (i : ℕ),
            AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
              u)
have mpr₂ : 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)
Tactic: refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩
-- 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
⊢ v ∩ u ∈ 𝓝[insert x s] x
have apply : v ∈ 𝓝[insert x s] x
Tactic: apply Filter.inter_mem _ hu
-- 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
⊢ v ∈ 𝓝[insert x s] x
have a : v ∈ 𝓝[u] x
Tactic: apply nhdsWithin_le_of_mem hu
-- 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.{u, uE, uF} (𝕜 := 𝕜) (n + 1) f (fun (x : E) ↦ (p' x).unshift (f x)) (v ∩ u)
have mpr : (∀ x ∈ v ∩ u, ContinuousMultilinearMap.curry0 ((p' x).unshift (f x) 0) = f x) ∧
  (∀ x ∈ v ∩ u,
      HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
        (fun (y : E) ↦ (p' y).unshift (f y) 0)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' x).unshift (f x) 1)) (v ∩ u) 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).unshift (f x) 1))
      (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
Tactic: rw [hasFTaylorSeriesUpToOn_succ_iff_right]
-- 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
⊢ (∀ x ∈ v ∩ u, ContinuousMultilinearMap.curry0 ((p' x).unshift (f x) 0) = f x) ∧
    (∀ x ∈ v ∩ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
          (fun (y : E) ↦ (p' y).unshift (f y) 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' x).unshift (f x) 1)) (v ∩ u) 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).unshift (f x) 1))
        (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
have mpr : ∀ (y : E) (hy : y ∈ v ∩ u),
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (y : E) ↦ (p' y).unshift (f y) 0)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1)) (v ∩ u) y
Tactic: refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩
-- 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
mpr :
  ∀ (y : E) (hy : y ∈ v ∩ u),
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (fun (y : E) ↦ (p' y).unshift (f y) 0)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1)) (v ∩ u) y
⊢ (∀ x ∈ v ∩ u, ContinuousMultilinearMap.curry0 ((p' x).unshift (f x) 0) = f x) ∧
    (∀ x ∈ v ∩ u,
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
          (fun (y : E) ↦ (p' y).unshift (f y) 0)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' x).unshift (f x) 1)) (v ∩ u) 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).unshift (f x) 1))
        (fun (x : E) ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
have mpr₁ : 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)
Tactic: refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩
-- 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
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (fun (z : E) ↦
      (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f z))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) ((p' y).unshift (f y) 1)) (v ∩ u) y
have mpr : HasFDerivWithinAt 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))
  (v ∩ u) y
Tactic: rw [← Function.comp_def _ f, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
-- 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
⊢ HasFDerivWithinAt 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))
    (v ∩ u) y
have h : (↑(↑(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) =
  f' y
Tactic: convert! (f'_eq_deriv y hy.2).mono inter_subset_right
-- 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
⊢ (↑(↑(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) =
    f' y
have h : (↑(↑(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) =
  ContinuousMultilinearMap.curry0 (p' y 0)
Tactic: rw [← Hp'.zero_eq y hy.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
y : E
hy : y ∈ v ∩ u
⊢ (↑(↑(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) =
    ContinuousMultilinearMap.curry0 (p' y 0)
have h : ∀ (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)
Tactic: ext z