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
n : ℕ∞ω
h :
  ∀ x ∈ s,
    ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f s x
have rcases : ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
  (hu : ContDiffOn 𝕜 n f (s ∩ u)), ContDiffWithinAt 𝕜 n f s x
Tactic: rcases h x xs with ⟨u, u_open, xu, 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
n : ℕ∞ω
h :
  ∀ x ∈ s,
    ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 n f s x
have apply : u ∈ 𝓝 x
Tactic: apply (contDiffWithinAt_inter _).1 (hu x ⟨xs, xu⟩)
-- 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
n : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    ∀ x ∈ s,
      ∃ u ∈ 𝓝[insert x s] x,
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have mp : ContDiffOn 𝕜 (n + 1) f s →
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
Tactic: constructor
-- 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
n : ℕ∞ω
hn : n ≠ ∞
mp :
  ContDiffOn 𝕜 (n + 1) f s →
    ∀ x ∈ s,
      ∃ u ∈ 𝓝[insert x s] x,
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    ∀ x ∈ s,
      ∃ u ∈ 𝓝[insert x s] x,
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have mpr : (∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u) →
  ContDiffOn 𝕜 (n + 1) f s
Tactic: constructor
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have mp : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (f_an : n = ω → AnalyticOn 𝕜 f u) (f' : E → E →L[𝕜] F)
  (hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) (Hf' : ContDiffWithinAt 𝕜 n f' u x),
  ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
Tactic: rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).1 (h x hx) with
      ⟨u, hu, f_an, f', hf', 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have mp : ∀ (v : Set E) (vu : v ∈ 𝓝[insert x u] x) (v'u : v ⊆ insert x u) (hv : ContDiffOn 𝕜 n f' v),
  ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
Tactic: rcases Hf'.contDiffOn le_rfl (by simp [hn]) with ⟨v, vu, v'u, hv⟩
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have mp : ∀ (hu : u ∈ 𝓝[s] x) (f_an : n = ω → AnalyticOn 𝕜 f u) (f' : E → E →L[𝕜] F)
  (hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) (Hf' : ContDiffWithinAt 𝕜 n f' u x) (v : Set E)
  (vu : v ∈ 𝓝[insert x u] x) (v'u : v ⊆ insert x u) (hv : ContDiffOn 𝕜 n f' v),
  ∃ u ∈ 𝓝[s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
Tactic: rw [insert_eq_of_mem hx] at hu ⊢
Cleared hypotheses: hu, f_an, f', hf', Hf', v, vu, v'u, hv
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
⊢ ∃ u ∈ 𝓝[s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have xu : x ∈ u
Tactic: have xu : x ∈ u := mem_of_mem_nhdsWithin hx hu
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
xu : x ∈ u
⊢ ∃ u ∈ 𝓝[s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have vu₁ : v ∈ 𝓝[u] x
Tactic: rw [insert_eq_of_mem xu] at vu v'u
Cleared hypotheses: vu, v'u, hv, xu
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
xu : x ∈ u
vu₁ : v ∈ 𝓝[u] x
⊢ ∃ u ∈ 𝓝[s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
have v'u₁ : v ⊆ u
Tactic: rw [insert_eq_of_mem xu] at vu v'u
Cleared hypotheses: vu, v'u, hv, xu
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x
have mpr : ∃ u ∈ 𝓝[insert x s] x,
  (n = ω → AnalyticOn 𝕜 f u) ∧
    ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
Tactic: rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn]
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
have mpr : ∀ (u : Set E) (u_nhbd : u ∈ 𝓝[insert x s] x) (f_an : n = ω → AnalyticOn 𝕜 f u) (f' : E → E →L[𝕜] F)
  (hu : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) (hf' : ContDiffOn 𝕜 n f' u),
  ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
Tactic: rcases h x hx with ⟨u, u_nhbd, f_an, f', hu, hf'⟩
-- 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
n : ℕ∞ω
hn : n ≠ ∞
h :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
u : Set E
u_nhbd : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hu : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffOn 𝕜 n f' u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
have this : x ∈ u
Tactic: have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert _ _) u_nhbd
-- 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
⊢ ContDiffOn 𝕜 0 f s ↔ ContinuousOn f s
have refine : ∀ (H : ContinuousOn f s) (x : E) (hx : x ∈ s) (m : ℕ) (hm : LE.le (α := ℕ∞) (↑m : ℕ∞) 0),
  ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
Tactic: refine ⟨fun H => H.continuousOn, fun H => fun x hx m hm ↦ ?_⟩
-- 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
H : ContinuousOn f s
x : E
hx : x ∈ s
m : ℕ
hm : LE.le (α := ℕ∞) (↑m : ℕ∞) 0
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
have this : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) 0
Tactic: have : (m : ℕ∞ω) = 0 := le_antisymm (mod_cast hm) bot_le
-- 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
H : ContinuousOn f s
x : E
hx : x ∈ s
m : ℕ
hm : LE.le (α := ℕ∞) (↑m : ℕ∞) 0
this : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) 0
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
have rw : ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn 0 f p u
Tactic: rw [this]
-- 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
H : ContinuousOn f s
x : E
hx : x ∈ s
m : ℕ
hm : LE.le (α := ℕ∞) (↑m : ℕ∞) 0
this : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) 0
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn 0 f p u
have refine : HasFTaylorSeriesUpToOn 0 f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
Tactic: refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_⟩
-- 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
H : ContinuousOn f s
x : E
hx : x ∈ s
m : ℕ
hm : LE.le (α := ℕ∞) (↑m : ℕ∞) 0
this : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) 0
⊢ HasFTaylorSeriesUpToOn 0 f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
have rw : ContinuousOn f (insert x s) ∧
  ∀ x_1 ∈ insert x s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x_1 0) = f x_1
Tactic: rw [hasFTaylorSeriesUpToOn_zero_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
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 0 f s x ↔ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
have mp : ContDiffWithinAt 𝕜 0 f s x → ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
Tactic: constructor
-- 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
hx : x ∈ s
mp : ContDiffWithinAt 𝕜 0 f s x → ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 0 f s x ↔ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
have mpr : (∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)) → ContDiffWithinAt 𝕜 0 f s x
Tactic: constructor
-- 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
hx : x ∈ s
h : ContDiffWithinAt 𝕜 0 f s x
⊢ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
have mp : ∀ (u : Set E) (H : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
  (hp : HasFTaylorSeriesUpToOn (↑0 : ℕ∞ω) f p u), ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
Tactic: obtain ⟨u, H, p, hp⟩ := h 0 le_rfl
-- 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
hx : x ∈ s
h : ContDiffWithinAt 𝕜 0 f s x
u : Set E
H : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑0 : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
have mp : u ∈ 𝓝[s] x
Tactic: refine ⟨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
hx : x ∈ s
h : ContDiffWithinAt 𝕜 0 f s x
u : Set E
H : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑0 : ℕ∞ω) f p u
mp : u ∈ 𝓝[s] x
⊢ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
have mp₁ : ContinuousOn f (s ∩ u)
Tactic: refine ⟨u, ?_, ?_⟩
-- 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
hx : x ∈ s
h : ContDiffWithinAt 𝕜 0 f s x
u : Set E
H : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑0 : ℕ∞ω) f p u
⊢ ContinuousOn f (s ∩ u)
have hp₁ : ContinuousOn f u ∧ ∀ x ∈ u, ContinuousMultilinearMap.curry0 (p x 0) = f x
Tactic: simp only [Nat.cast_zero, hasFTaylorSeriesUpToOn_zero_iff] at hp
Cleared hypotheses: hp
-- 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
hx : x ∈ s
u : Set E
H : u ∈ 𝓝[s] x
hu : ContinuousOn f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 0 f s x
have mpr : ContDiffWithinAt 𝕜 0 f (s ∩ u) x
Tactic: rw [← contDiffWithinAt_inter' H]
-- 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
hx : x ∈ s
u : Set E
H : u ∈ 𝓝[s] x
hu : ContinuousOn f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 0 f (s ∩ u) x
have h' : x ∈ s ∩ u
Tactic: have h' : x ∈ s ∩ u := ⟨hx, mem_of_mem_nhdsWithin hx 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
have zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
Tactic: constructor
-- 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
have fderivWithin : ∀ (m : ℕ),
  (↑m : ℕ∞ω) < n →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
Tactic: constructor
-- 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
have cont : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ n →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) s
Tactic: constructor
-- 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 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) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
have this : (↑(m + 1) : ℕ∞ω) ≤ n
Tactic: have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hm
-- 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
have fderivWithin : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
  (Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u),
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
Tactic: rcases (h x hx).of_le this _ le_rfl with ⟨u, hu, p, Hp⟩
-- 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
have fderivWithin : ∀ (hu : u ∈ 𝓝[s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u),
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
Tactic: rw [insert_eq_of_mem hx] at hu
Cleared hypotheses: hu, p, Hp