awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : w ∩ insert x s ⊆ u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have hwu₁ : insert x s ∩ w ⊆ u
Tactic: rw [inter_comm] at hwu
Cleared hypotheses: hwu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : insert x s ∩ w ⊆ u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_1 : n = ω → AnalyticOn 𝕜 f (insert x s ∩ w)
Tactic: refine ⟨insert x s ∩ w, inter_mem_nhdsWithin _ (hw.mem_nhds hxw), inter_subset_left, ?_, f',
      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 ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : insert x s ∩ w ⊆ u
refine_1 : n = ω → AnalyticOn 𝕜 f (insert x s ∩ w)
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_1₁ : ∀ (y : E) (hy : y ∈ insert x s ∩ w), HasFDerivWithinAt f (f' y) s y
Tactic: refine ⟨insert x s ∩ w, inter_mem_nhdsWithin _ (hw.mem_nhds hxw), inter_subset_left, ?_, f',
      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 ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : insert x s ∩ w ⊆ u
refine_1 : n = ω → AnalyticOn 𝕜 f (insert x s ∩ w)
refine_1₁ : ∀ (y : E) (hy : y ∈ insert x s ∩ w), HasFDerivWithinAt f (f' y) s y
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
have refine_1₂ : ContDiffWithinAt 𝕜 n f' s x
Tactic: refine ⟨insert x s ∩ w, inter_mem_nhdsWithin _ (hw.mem_nhds hxw), inter_subset_left, ?_, f',
      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 ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : insert x s ∩ w ⊆ u
y : E
hy : y ∈ insert x s ∩ w
⊢ HasFDerivWithinAt f (f' y) s y
have refine_1 : insert x s ∩ w ∈ 𝓝[s] y
Tactic: refine ((huf' y <| hwu hy).mono hwu).mono_of_mem_nhdsWithin ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : insert x s ∩ w ⊆ u
y : E
hy : y ∈ insert x s ∩ w
⊢ insert x s ∩ w ∈ 𝓝[s] y
have refine_1 : s ∩ w ∈ 𝓝[s] y
Tactic: grw [← subset_insert]
-- 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 ≠ ∞
⊢ (∃ u ∈ 𝓝[insert x s] x,
      u ⊆ insert x s ∧
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
    ContDiffWithinAt 𝕜 (n + 1) f s x
have refine_2 : (∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x) →
  ∃ 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_insert, contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,
      insert_eq_of_mem (mem_insert _ _)]
-- 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 : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
have h : s ∈ 𝓝[insert x s] x ∧ ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p s
Tactic: use 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
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ s ∈ 𝓝[insert x s] x ∧ ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p s
have h : ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p s
Tactic: simp only [Set.insert_eq_of_mem hx, self_mem_nhdsWithin, true_and]
-- 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
m n : ℕ∞ω
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
have inl : ∀ (hm : m ≤ ω) (h' : m = ∞ → Eq (α := ℕ∞ω) ω ω) (h : ContDiffWithinAt 𝕜 ω f s x),
  ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
Tactic: rcases eq_or_ne n ω with rfl | hn
Cleared hypotheses: n, hm, h', h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m n : ℕ∞ω
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
inl :
  ∀ (hm : m ≤ ω) (h' : m = ∞ → Eq (α := ℕ∞ω) ω ω) (h : ContDiffWithinAt 𝕜 ω f s x),
    ∃ (u : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
have inr : ∀ (hn : n ≠ ω),
  ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
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
x : E
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → Eq (α := ℕ∞ω) ω ω
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
have inl : ∀ (t : Set E) (ht : t ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p t)
  (h'p :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) t),
  ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
Tactic: obtain ⟨t, ht, p, hp, h'p⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → Eq (α := ℕ∞ω) ω ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) t
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
have inl : ∀ (u : Set E) (huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (hxu : x ∈ u)
  (hut : u ∩ insert x s ⊆ t),
  ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
Tactic: rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
-- 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
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → Eq (α := ℕ∞ω) ω ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : u ∩ insert x s ⊆ t
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
have hut₁ : insert x s ∩ u ⊆ t
Tactic: rw [inter_comm] at hut
Cleared hypotheses: hut
-- 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
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → Eq (α := ℕ∞ω) ω ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
have inl : ContDiffOn 𝕜 m f (insert x s ∩ u)
Tactic: refine ⟨u, huo, hxu, ?_⟩
-- 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
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → Eq (α := ℕ∞ω) ω ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ContDiffOn 𝕜 m f (insert x s ∩ u)
have inl : ContDiffOn 𝕜 ω f (insert x s ∩ u)
Tactic: suffices ContDiffOn 𝕜 ω f (insert x s ∩ u) 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
x : E
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → Eq (α := ℕ∞ω) ω ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
y : E
hy : y ∈ insert x s ∩ u
⊢ ContDiffWithinAt 𝕜 ω f (insert x s ∩ u) y
have inl : insert x s ∩ u ∈ 𝓝[insert y (insert x s ∩ u)] y
Tactic: refine ⟨insert x s ∩ u, ?_, p, hp.mono hut, fun i ↦ (h'p i).mono hut⟩
-- 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
m_1 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert x s ∩ u)
have rcases : ∀ (t : Set E) (ht : t ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
  (hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p t),
  ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert x s ∩ u)
Tactic: rcases contDiffWithinAt_nat.1 (h.of_le hm) with ⟨t, ht, 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
x : E
m_1 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p t
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert x s ∩ u)
have rcases : ∀ (u : Set E) (huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (hxu : x ∈ u)
  (hut : u ∩ insert x s ⊆ t),
  ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert x s ∩ u)
Tactic: rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
-- 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
m_1 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : u ∩ insert x s ⊆ t
⊢ ∃ (u : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert x s ∩ u)
have hut₁ : insert x s ∩ u ⊆ t
Tactic: rw [inter_comm] at hut
Cleared hypotheses: hut
-- 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
m n : ℕ∞ω
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u
have obtain : ∀ (_u : Set E) (uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] _u) (xu : x ∈ _u)
  (h : ContDiffOn 𝕜 m f (insert x s ∩ _u)), ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u
Tactic: obtain ⟨_u, uo, xu, h⟩ := h.contDiffOn' hm h'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
have refine_1 : ∀ (h : ContDiffWithinAt 𝕜 n f s x), ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
refine_1 : ∀ (h : ContDiffWithinAt 𝕜 n f s x), ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
have refine_2 : ∀ (h : ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u), ContDiffWithinAt 𝕜 n f s x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
have refine_1 : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (h'u : u ⊆ insert x s ∧ ContDiffOn 𝕜 n f u),
  ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
Tactic: rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, h'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
n : ℕ∞ω
hn : n ≠ ∞
h : ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
⊢ ContDiffWithinAt 𝕜 n f s x
have refine_2 : ∀ (u : Set E) (u_mem : u ∈ 𝓝[insert x s] x) (hu : ContDiffOn 𝕜 n f u), ContDiffWithinAt 𝕜 n f s x
Tactic: rcases h with ⟨u, u_mem, hu⟩
Cleared hypotheses: 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
n : ℕ∞ω
hn : n ≠ ∞
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
hu : ContDiffOn 𝕜 n f u
⊢ ContDiffWithinAt 𝕜 n f s x
have this : x ∈ u
Tactic: have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert x s) u_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
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y
have rcases : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x),
  u ⊆ insert x s → ∀ (hd : ContDiffOn 𝕜 n f u), ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y
Tactic: rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, _, hd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y
have this : ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u
Tactic: have : ∀ᶠ y : E in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u :=
    (eventually_eventually_nhdsWithin.2 hu).and 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 : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
this : ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y
have refine : ∀ (y : E) (hy : u ∈ 𝓝[insert x s] y ∧ y ∈ u), u ∈ 𝓝[s] y
Tactic: refine this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_
-- 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 : ℕ∞), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
have refine : (∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s) → ∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
Tactic: refine ⟨fun H n => H n, ?_⟩