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 : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
inl :
  ∀ (h' : Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s)
    (h : ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fun (y : E) ↦ fderivWithin 𝕜 f s y) s),
    ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) f s
⊢ ContDiffOn 𝕜 (n + 1) f s
have inr : ∀ (hn : n ≠ ∞), ContDiffOn 𝕜 (n + 1) f s
Tactic: rcases eq_or_ne n ∞ with rfl | 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
hf : DifferentiableOn 𝕜 f s
h' : Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) f s
have inl : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
Tactic: rw [ENat.coe_top_add_one, contDiffOn_infty]
-- 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
hf : DifferentiableOn 𝕜 f s
h' : Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f s x
have apply : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1) f s x
Tactic: apply ContDiffWithinAt.of_le _ (show (m : ℕ∞ω) ≤ m + 1 from le_self_add)
-- 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
hf : DifferentiableOn 𝕜 f s
h' : Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1) f s x
have rw : ∃ u ∈ 𝓝[s] x,
  (Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
    ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
Tactic: rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp),
      insert_eq_of_mem hx]
-- 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 : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x
have inr : ∃ u ∈ 𝓝[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,
      insert_eq_of_mem hx]
-- 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 : ℕ∞ω
hf : AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) ω (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 n f s
have suffices : ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ω 1) f s
Tactic: suffices ContDiffOn 𝕜 (ω + 1) f s from this.of_le le_top
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
have refine : ∀ (H : ContDiffOn 𝕜 (n + 1) f s),
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
Tactic: refine ⟨fun H => ?_, fun h => contDiffOn_succ_of_fderivWithin h.1 h.2.1 h.2.2⟩
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
have refine_1 : n = ω → AnalyticOn 𝕜 f s
Tactic: refine ⟨H.differentiableOn (by simp), ?_, fun x hx => ?_⟩
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
refine_1 : n = ω → AnalyticOn 𝕜 f s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
have refine_2 : ∀ (x : E) (hx : x ∈ s), ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s x
Tactic: refine ⟨H.differentiableOn (by simp), ?_, fun x hx => ?_⟩
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
have rcases : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (f' : E → E →L[𝕜] F) (hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x)
  (hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x),
  ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
Tactic: rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt (n := m) (ne_of_beq_false rfl)).1
      (H.of_le (by gcongr) x hx) with ⟨u, hu, -, f', hff', 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
have rcases : ∀ (o : Set E) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o) (xo : x ∈ o)
  (ho : o ∩ insert x s ⊆ u), ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
Tactic: rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ insert x s ⊆ u
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
have ho₁ : s ∩ o ⊆ u
Tactic: rw [inter_comm, insert_eq_of_mem hx] at ho
Cleared hypotheses: ho
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
have this : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' (s ∩ o) x
Tactic: have := hf'.mono ho
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' (s ∩ o) x
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
have this₁ : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
Tactic: rw [contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds o_open xo))] at this
Cleared hypotheses: 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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
have apply : (fun (y : E) ↦ fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'
Tactic: apply this.congr_of_eventuallyEq_of_mem _ hx
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
⊢ (fun (y : E) ↦ fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'
have this₁ : o ∩ s ∈ 𝓝[s] x
Tactic: have : o ∩ s ∈ 𝓝[s] x := mem_nhdsWithin.2 ⟨o, o_open, xo, Subset.refl _⟩
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this_1 : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
this : o ∩ s ∈ 𝓝[s] x
⊢ (fun (y : E) ↦ fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'
have this₁ : s ∩ o ∈ 𝓝[s] x
Tactic: rw [inter_comm] at this
Cleared hypotheses: 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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this_1 : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
this : s ∩ o ∈ 𝓝[s] x
⊢ (fun (y : E) ↦ fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'
have refine : ∀ (y : E) (hy : y ∈ s ∩ o), fderivWithin 𝕜 f s y = f' y
Tactic: refine Filter.eventuallyEq_of_mem this fun y hy => ?_
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this_1 : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
this : s ∩ o ∈ 𝓝[s] x
y : E
hy : y ∈ s ∩ o
⊢ fderivWithin 𝕜 f s y = f' y
have A : fderivWithin 𝕜 f (s ∩ o) y = f' y
Tactic: have A : fderivWithin 𝕜 f (s ∩ o) y = f' y :=
      ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter o_open 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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this_1 : ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f' s x
this : s ∩ o ∈ 𝓝[s] x
y : E
hy : y ∈ s ∩ o
A : fderivWithin 𝕜 f (s ∩ o) y = f' y
⊢ fderivWithin 𝕜 f s y = f' y
have rwa : ∀ (A : fderivWithin 𝕜 f s y = f' y), fderivWithin 𝕜 f s y = f' y
Tactic: rwa [fderivWithin_inter (o_open.mem_nhds hy.2)] at A
Cleared hypotheses: A
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s x
have A : ∀ (m : ℕ) (hm : (↑m : ℕ∞ω) ≤ n), ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) (↑m : ℕ∞ω) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x
Tactic: have A (m : ℕ) (hm : m ≤ n) : ContDiffWithinAt 𝕜 m (fun y => fderivWithin 𝕜 f s y) s x := by
    rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt (n := m) (ne_of_beq_false rfl)).1
      (H.of_le (by gcongr) x hx) with ⟨u, hu, -, f', hff', hf'⟩
    rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
    rw [inter_comm, insert_eq_of_mem hx] at ho
    have := hf'.mono ho
    rw [contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds o_open xo))] at this
    apply this.congr_of_eventuallyEq_of_mem _ hx
    have : o ∩ s ∈ 𝓝[s] x := mem_nhdsWithin.2 ⟨o, o_open, xo, Subset.refl _⟩
    rw [inter_comm] at this
    refine Filter.eventuallyEq_of_mem this fun y hy => ?_
    have A : fderivWithin 𝕜 f (s ∩ o) y = f' y :=
      ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter o_open y hy)
    rwa [fderivWithin_inter (o_open.mem_nhds hy.2)] at A
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
have rw : DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s ↔
  (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
Tactic: rw [contDiffOn_succ_iff_fderivWithin hs]
-- 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s ↔
    (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
have refine : ((n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
  ∀ (f_an : n = ω → AnalyticOn 𝕜 f s)
    (h : ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x),
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
Tactic: refine ⟨fun h => ⟨h.2.1, fderivWithin 𝕜 f s, h.2.2,
    fun x hx => (h.1 x hx).hasFDerivWithinAt⟩, fun ⟨f_an, 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
h_1 : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
h : ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
have rcases : ∀ (f' : E → E →L[𝕜] F) (h1 : ContDiffOn 𝕜 n f' s) (h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x),
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
Tactic: rcases h with ⟨f', h1, h2⟩
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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
h : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
f' : E → E →L[𝕜] F
h1 : ContDiffOn 𝕜 n f' s
h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
have refine : ∀ (x : E) (hx : x ∈ s), ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s x
Tactic: refine ⟨fun x hx => (h2 x hx).differentiableWithinAt, f_an, fun x hx => ?_⟩
-- 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
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderivWithin 𝕜 f s) s
have rw : DifferentiableOn 𝕜 f s ∧
    (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderivWithin 𝕜 f s) s ↔
  DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderivWithin 𝕜 f s) s
Tactic: rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin hs]
-- 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 : ℕ∞ω
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
have rw : DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s ↔
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
Tactic: rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
    contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]
-- 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 : ℕ∞ω
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw :
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
have rw₁ : DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fun (x : E) ↦ fderiv 𝕜 f x) s ↔
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
Tactic: rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
    contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f) s
have rw : DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f) s ↔
  DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderiv 𝕜 f) s
Tactic: rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]
-- 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
⊢ ContDiffAt 𝕜 n f x
have rwa : ContDiffWithinAt 𝕜 n f univ x
Tactic: rwa [ContDiffAt, ← contDiffWithinAt_inter hx, univ_inter]