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 : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) 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 rw : ∃ u ∈ 𝓝[s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
Tactic: rw [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 : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
have refine : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) s
Tactic: refine ⟨s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) s
have zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) s
have fderivWithin : ∀ (m_1 : ℕ),
  LT.lt (α := ℕ∞ω) (↑m_1 : ℕ∞ω) (↑m : ℕ∞ω) →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m_1) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m_1)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m_1.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m_1.succ)) s
        x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < n →
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : (↑m : ℕ∞) ≤ n
zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
fderivWithin :
  ∀ (m_1 : ℕ),
    LT.lt (α := ℕ∞ω) (↑m_1 : ℕ∞ω) (↑m : ℕ∞ω) →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m_1) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m_1)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m_1.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m_1.succ))
          s x
⊢ HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) s
have cont : ∀ (m_1 : ℕ),
  LE.le (α := ℕ∞ω) (↑m_1 : ℕ∞ω) (↑m : ℕ∞ω) →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m_1) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m_1) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      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 :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x
have refine_1 : HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
Tactic: refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
refine_1 : HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
⊢ ContDiffWithinAt 𝕜 ω f s x
have refine_2 : ∀ (i : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)
Tactic: refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
have refine_1 : HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) s
Tactic: rw [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 : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) s
have refine_1 : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
refine_1 : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) s
have refine_1₁ : ∀ (m : ℕ),
  LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) ω →
    ∀ x ∈ s,
      HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
refine_1 : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
refine_1₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) ω →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) s
have refine_1₂ : ∀ (m : ℕ),
  LE.le (α := ℕ∞ω) (↑m : ℕ∞ω) ω →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (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 :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDerivWithin 𝕜 m f s)
      s
x : E
hx : x ∈ s
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) (insert x s)
have refine_2 : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
  (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x i) s
Tactic: rw [insert_eq_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 : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have this : (↑(m + 1) : ℕ∞ω) ≤ n
Tactic: have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hmn
-- 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 : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : (↑(m + 1) : ℕ∞ω) ≤ n
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have apply : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑(m + 1) : ℕ∞ω)
Tactic: apply (((h.of_le this).ftaylorSeriesWithin hs).fderivWithin m ?_ x hx).differentiableWithinAt
-- 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 : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
Tactic: have : (m + 1 : ℕ∞ω) ≠ ∞ := Ne.symm (ne_of_beq_false rfl)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have rcases : ∀ (u : Set E) (uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
  (hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f (insert x s ∩ u)),
  DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
Tactic: rcases h.contDiffOn' (ENat.add_one_natCast_le_withTop_of_lt hmn) (by simp [this])
    with ⟨u, uo, 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 : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
⊢ t =ᶠ[𝓝[≠] x] s
have simp : 𝓝[{x}ᶜ ∩ t] x = 𝓝[{x}ᶜ ∩ s] x
Tactic: simp only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_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 : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
⊢ 𝓝[{x}ᶜ ∩ t] x = 𝓝[{x}ᶜ ∩ s] x
have h₁ : Membership.mem (γ := Set E) {x} x
Tactic: rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem,
      diff_eq_compl_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 : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
h₁ : Membership.mem (γ := Set E) {x} x
⊢ 𝓝[{x}ᶜ ∩ t] x = 𝓝[{x}ᶜ ∩ s] x
have rw : u ∈ 𝓝[{x}ᶜ ∩ insert x s] x
Tactic: rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem,
      diff_eq_compl_inter]
-- 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 : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have A : t =ᶠ[𝓝[≠] x] s
Tactic: have A : t =ᶠ[𝓝[≠] x] s := by
    simp only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter']
    rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem,
      diff_eq_compl_inter]
    exacts [rfl, mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
A : t =ᶠ[𝓝[≠] x] s
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have B : (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
  (iteratedFDerivWithin 𝕜 m f s) (iteratedFDerivWithin 𝕜 m f t)
Tactic: have B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t :=
    iteratedFDerivWithin_eventually_congr_set' _ A.symm _
-- 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 : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
A : t =ᶠ[𝓝[≠] x] s
B :
  (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) (iteratedFDerivWithin 𝕜 m f t)
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have C : DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
  (iteratedFDerivWithin 𝕜 m f t) t x
Tactic: have C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) t x :=
    hu.differentiableOn_iteratedFDerivWithin (Nat.cast_lt.2 m.lt_succ_self) (hs.inter uo) x
      ⟨mem_insert _ _, xu⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : (↑m : ℕ∞ω) < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t
A : t =ᶠ[𝓝[≠] x] s
B :
  (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) (iteratedFDerivWithin 𝕜 m f t)
C :
  DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f t) t x
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x
have C₁ : DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
  (iteratedFDerivWithin 𝕜 m f t) s x
Tactic: rw [differentiableWithinAt_congr_set' _ A] at C
Cleared hypotheses: C
-- 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 : ℕ∞ω) f s ↔
    (∀ m ≤ n,
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n,
        DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
have rw : ((∀ (m : ℕ),
      LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) →
        ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
    ∀ (m : ℕ),
      LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) →
        DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
          (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s) ↔
  (∀ m ≤ n,
      ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
    ∀ m < n,
      DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fun (x : E) ↦ iteratedFDerivWithin 𝕜 m f s x) s
Tactic: rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn 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 : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 (n + 1) f s
have 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
Tactic: rcases eq_or_ne n ∞ with rfl | hn
Cleared hypotheses: n, h', h