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 : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
rwa : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffAt 𝕜 n f x
have rwa₁ : ContDiffWithinAt 𝕜 n f (univ ∩ s) x
Tactic: rwa [ContDiffAt, ← contDiffWithinAt_inter hx, univ_inter]
-- 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 : ℕ∞ω
h : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x
have rw : ContDiffWithinAt 𝕜 n f (univ ∩ s) x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_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 : ℕ∞ω
h : s ∈ 𝓝 x
rw : ContDiffWithinAt 𝕜 n f (univ ∩ s) x ↔ ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x
have rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_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 : ℕ∞ω
h : s ∈ 𝓝 x
rw : ContDiffWithinAt 𝕜 n f (univ ∩ s) x ↔ ContDiffAt 𝕜 n f x
rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x
have rw₂ : ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_univ]
-- 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
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
⊢ AnalyticAt 𝕜 f x
have h₁ : ContDiffWithinAt 𝕜 ω f univ x
Tactic: rw [← contDiffWithinAt_univ] 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
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticAt 𝕜 f x
have rw : AnalyticWithinAt 𝕜 f univ x
Tactic: rw [← analyticWithinAt_univ]
-- 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
f : E → F
x : E
n : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ ContDiffWithinAt 𝕜 n f univ x
have h₁ : AnalyticWithinAt 𝕜 f univ x
Tactic: rw [← analyticWithinAt_univ] 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
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x
have rw : ContDiffWithinAt 𝕜 n f (univ \ {x}) x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [compl_eq_univ_diff, contDiffWithinAt_diff_singleton, contDiffWithinAt_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
f : E → F
x : E
n : ℕ∞ω
rw : ContDiffWithinAt 𝕜 n f (univ \ {x}) x ↔ ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x
have rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [compl_eq_univ_diff, contDiffWithinAt_diff_singleton, contDiffWithinAt_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
f : E → F
x : E
n : ℕ∞ω
rw : ContDiffWithinAt 𝕜 n f (univ \ {x}) x ↔ ContDiffAt 𝕜 n f x
rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x
have rw₂ : ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [compl_eq_univ_diff, contDiffWithinAt_diff_singleton, contDiffWithinAt_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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f) x
have rw : DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f)
  univ x
Tactic: rw [← differentiableWithinAt_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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDeriv 𝕜 m f) univ x
have h₁ : Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f)
  (iteratedFDerivWithin 𝕜 m f univ)
Tactic: convert! (h.differentiableWithinAt_iteratedFDerivWithin hmn (by simp [uniqueDiffOn_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
f : E → F
x : E
n : ℕ
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
have rw : (∃ u ∈ 𝓝[insert x univ] x,
    (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
  ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
Tactic: rw [← contDiffWithinAt_univ, contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp)]
-- 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
f : E → F
x : E
n : ℕ
⊢ (∃ u ∈ 𝓝[insert x univ] x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
have simp : (∃ u ∈ 𝓝 x,
    (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
  ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
Tactic: simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem]
-- 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
f : E → F
x : E
n : ℕ
⊢ (∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
have mp : (∃ u ∈ 𝓝 x,
    (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) →
  ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) 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
f : E → F
x : E
n : ℕ
mp :
  (∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) →
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
⊢ (∃ u ∈ 𝓝 x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
have mpr : (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x) →
  ∃ u ∈ 𝓝 x,
    (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
⊢ ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
have mp : ∀ (t : Set E) (htu : t ⊆ u) (ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (hxt : x ∈ t),
  ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
Tactic: rcases mem_nhds_iff.mp H with ⟨t, htu, ht, hxt⟩
-- 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
⊢ ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
have mp : t ∈ 𝓝 x ∧ ∀ x ∈ t, HasFDerivAt f (f' x) x
Tactic: refine ⟨f', ⟨t, ?_⟩, h_cont_diff.contDiffAt 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
⊢ t ∈ 𝓝 x ∧ ∀ x ∈ t, HasFDerivAt f (f' x) x
have mp : ∀ x ∈ t, HasFDerivAt f (f' x) x
Tactic: refine ⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩
-- 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
f : E → F
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
y : E
hyt : y ∈ t
⊢ HasFDerivAt f (f' y) y
have mp : u ∈ 𝓝 y
Tactic: refine (h_fderiv y (htu hyt)).hasFDerivAt ?_
-- 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
f : E → F
x : E
n : ℕ
f' : E → E →L[𝕜] F
h_cont_diff : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
u : Set E
H : u ∈ 𝓝 x
h_fderiv : ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ ∃ u ∈ 𝓝 x,
    (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
      ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x
have mpr : ∀ (x : E) (hxu : x ∈ u), HasFDerivWithinAt f (f' x) u x
Tactic: refine ⟨u, H, by simp, f', fun x hxu ↦ ?_, h_cont_diff.contDiffWithinAt⟩
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDeriv 𝕜 n f x)
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
  (iteratedFDerivWithin 𝕜 n f univ x)
Tactic: rw [← iteratedFDerivWithin_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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)
have rcases : ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
  (hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)),
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)
Tactic: rcases h.contDiffOn' le_rfl (by simp) 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
  (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
Tactic: rw [← iteratedFDerivWithin_inter_open u_open xu,
    ← iteratedFDerivWithin_inter_open u_open xu (s := 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
have st : s ∩ u ⊆ univ ∩ u
Tactic: apply iteratedFDerivWithin_subset
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
st : s ∩ u ⊆ univ ∩ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
have hs₁ : UniqueDiffOn 𝕜 (s ∩ u)
Tactic: apply iteratedFDerivWithin_subset
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
st : s ∩ u ⊆ univ ∩ u
hs₁ : UniqueDiffOn 𝕜 (s ∩ u)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
have ht : UniqueDiffOn 𝕜 (univ ∩ u)
Tactic: apply iteratedFDerivWithin_subset
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
st : s ∩ u ⊆ univ ∩ u
hs₁ : UniqueDiffOn 𝕜 (s ∩ u)
ht : UniqueDiffOn 𝕜 (univ ∩ u)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
have h₁ : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (univ ∩ u)
Tactic: apply iteratedFDerivWithin_subset
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n : ℕ∞ω) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (insert x univ ∩ u)
st : s ∩ u ⊆ univ ∩ u
hs₁ : UniqueDiffOn 𝕜 (s ∩ u)
ht : UniqueDiffOn 𝕜 (univ ∩ u)
h₁ : ContDiffOn 𝕜 (↑n : ℕ∞ω) f (univ ∩ u)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f (univ ∩ u) x)
have hx₁ : x ∈ s ∩ u
Tactic: apply iteratedFDerivWithin_subset
-- 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
f : E → F
n : ℕ∞ω
⊢ ContDiffOn 𝕜 ω f univ ↔ ContDiff 𝕜 ω f
have mp : ContDiffOn 𝕜 ω f univ → ContDiff 𝕜 ω f
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
f : E → F
n : ℕ∞ω
mp : ContDiffOn 𝕜 ω f univ → ContDiff 𝕜 ω f
⊢ ContDiffOn 𝕜 ω f univ ↔ ContDiff 𝕜 ω f
have mpr : ContDiff 𝕜 ω f → ContDiffOn 𝕜 ω f univ
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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ ContDiff 𝕜 ω f
have h : HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
  ∀ (i : ℕ),
    AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
Tactic: use ftaylorSeriesWithin 𝕜 f 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
have h : HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
  ∀ (i : ℕ),
    AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
Tactic: rw [← hasFTaylorSeriesUpToOn_univ_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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ),
      AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
have h : ∀ (i : ℕ),
  AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
Tactic: refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩
-- 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
have h : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
  (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
Tactic: rw [← analyticOn_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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ContDiff 𝕜 (↑n : ℕ∞ω) f
have mp : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → ContDiff 𝕜 (↑n : ℕ∞ω) f
Tactic: constructor