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 : 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 ∈ 𝓝[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 : ∀ (o : Set E) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o) (xo : x ∈ o) (ho : o ∩ s ⊆ 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 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 : ℕ∞ω
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 ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ s ⊆ 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 ho₁ : s ∩ o ⊆ u
Tactic: rw [inter_comm] at ho
Cleared hypotheses: ho
-- 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 ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (iteratedFDerivWithin 𝕜 m.succ f s x)
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
  (iteratedFDerivWithin 𝕜 m.succ f (s ∩ o) x)
Tactic: rw [← iteratedFDerivWithin_inter_open o_open xo]
-- 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
this : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ 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 this₁ : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
  (ftaylorSeriesWithin 𝕜 f s x m.succ)
Tactic: have : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ := by
      change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x
      rw [← iteratedFDerivWithin_inter_open o_open xo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
-- 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_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
⊢ 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 : 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) (p x m.succ)) (s ∩ o) x
Tactic: rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)]
-- 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_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y
have rw : p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y
Tactic: rw [← iteratedFDerivWithin_inter_open o_open yo]
-- 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
this_1 : (↑(m + 1) : ℕ∞ω) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1) : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
this :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F) (p x m.succ)
    (ftaylorSeriesWithin 𝕜 f s x m.succ)
⊢ 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) (p x m.succ)) (s ∩ o) x
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
Tactic: have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin 𝕜 m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact
        (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
          (hs.inter o_open) ⟨hy, yo⟩
-- 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
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) s
have cont : ∀ x ∈ s,
  ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
Tactic: apply continuousOn_of_locally_continuousOn
-- 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
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
have cont : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
  (Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
  ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
Tactic: rcases (h x hx).of_le hm _ 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
have cont : ∀ (o : Set E) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o) (xo : x ∈ o)
  (ho : o ∩ insert x s ⊆ u),
  ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ insert x s ⊆ u
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
have ho₁ : o ∩ s ⊆ u
Tactic: rw [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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ s ⊆ u
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
have ho₁ : s ∩ o ⊆ u
Tactic: rw [inter_comm] at ho
Cleared hypotheses: ho
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
have cont : ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
  (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)
Tactic: refine ⟨o, o_open, xo, ?_⟩
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y
have rw : p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y
Tactic: rw [← iteratedFDerivWithin_inter_open o_open yo]
-- 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
Tactic: have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin 𝕜 m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t
have rcases : ∀ (U : Set E) (hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (haU : a ∈ U)
  (hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)),
  ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t
Tactic: rcases h.contDiffOn' hm (by simp) with ⟨U, hUo, haU, hfU⟩
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
have rw : s ∩ U ∈ 𝓝[s] a
Tactic: rw [eventually_smallSets_subset]
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t
have this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
Tactic: have : ∀ᶠ t in (𝓝[s] a).smallSets, t ⊆ s ∩ U := by
    rw [eventually_smallSets_subset]
    exact inter_mem_nhdsWithin _ <| hUo.mem_nhds haU
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) t
have refine : ∀ (t : Set E) (ht : t ⊆ s ∩ U), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
Tactic: refine this.mono fun t ht ↦ .mono ?_ ht
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
have rw : ∀ (hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)) (this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U) (t : Set E)
  (ht : t ⊆ s ∩ U), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
Tactic: rw [insert_eq_of_mem ha] at hfU
Cleared hypotheses: hfU, this, t, ht
-- 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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m : ℕ∞ω) f (s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
have refine : ∀ (k : ℕ) (hk : LE.le (α := ℕ∞ω) (↑k : ℕ∞ω) (↑m : ℕ∞ω)) (x : E) (hx : x ∈ s ∩ U),
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((fun (x : E) ↦
        (ftaylorSeriesWithin 𝕜 f (s ∩ U) x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)
    ((fun (x : E) ↦ (ftaylorSeriesWithin 𝕜 f s x k : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)
Tactic: refine (hfU.ftaylorSeriesWithin (hs.inter hUo)).congr_series fun k hk 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 : ℕ∞ω
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 n f s
have suffices : ContDiffOn 𝕜 ω f s
Tactic: suffices ContDiffOn 𝕜 ω 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 : ℕ∞ω
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ω f s
have rcases : ∀ (p : E → FormalMultilinearSeries 𝕜 E F)
  (hp :
    HasFTaylorSeriesUpToOn ω f p s ∧
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s),
  ContDiffOn 𝕜 ω f s
Tactic: rcases h.exists_hasFTaylorSeriesUpToOn hs with ⟨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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x
have refine : s ∈ 𝓝[insert x s] x
Tactic: refine ⟨s, ?_, 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp :
  HasFTaylorSeriesUpToOn ω f p s ∧
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[insert x s] x
have rw : s ∈ 𝓝[s] x
Tactic: rw [insert_eq_of_mem hx]