awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑(m + 1) : ℕ∞ω)

Tactic:
exact_mod_cast lt_add_one m

Premises used: lt_add_one
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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)
⊢ HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1 ≠ ∞

Tactic:
have : (m + 1 : ℕ∞ω) ≠ ∞ := Ne.symm (ne_of_beq_false rfl)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 ≠ ∞
⊢ Eq (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) ∞ → n = ω

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 ≠ ∞
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
⊢ 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⟩

Premises used: ENat.add_one_natCast_le_withTop_of_lt, ContDiffWithinAt.contDiffOn'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
hu : ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f (insert x s ∩ u)
⊢ let t := insert x s ∩ u;
  ContDiffOn 𝕜 (↑(m + 1) : ℕ∞ω) f t

Tactic:
set t := insert x s ∩ u

Premises used: Insert.insert
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
simp : 𝓝[{x}ᶜ ∩ t] x = 𝓝[{x}ᶜ ∩ s] x
⊢ t =ᶠ[𝓝[≠] x] s

Tactic:
simp only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter']

Premises used: Filter.set_eventuallyEq_iff_inf_principal, nhdsWithin_inter'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
rw : u ∈ 𝓝[{x}ᶜ ∩ insert x s] x
⊢ 𝓝[{x}ᶜ ∩ t] x = 𝓝[{x}ᶜ ∩ s] x

Tactic:
rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem,
      diff_eq_compl_inter]

Premises used: Set.diff_eq_compl_inter, Set.insert_diff_of_mem, nhdsWithin_inter_of_mem', Set.inter_assoc
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ Membership.mem (γ := Set E) {x} x

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.singleton, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ u ∈ 𝓝[{x}ᶜ ∩ insert x s] x

Tactic:
mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)

Premises used: mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ Membership.mem (γ := Set E) {x} x

Tactic:
exacts [rfl, mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)]

Premises used: mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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

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)]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ (𝓝 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 _
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 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⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 t) s x

Tactic:
rw [differentiableWithinAt_congr_set' _ A] at C

Premises used: differentiableWithinAt_congr_set'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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) s x
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
C.congr_of_eventuallyEq (B.filter_mono inf_le_left) B.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, DifferentiableWithinAt.congr_of_eventuallyEq, inf_le_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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) s x
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
exact C.congr_of_eventuallyEq (B.filter_mono inf_le_left) B.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, DifferentiableWithinAt.congr_of_eventuallyEq, inf_le_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ),
        (↑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 : ℕ),
        (↑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:
⟨fun h => ⟨fun _m hm => h.continuousOn_iteratedFDerivWithin (mod_cast hm) hs,
      fun _m hm => h.differentiableOn_iteratedFDerivWithin (mod_cast hm) hs⟩,
    fun h => contDiffOn_of_continuousOn_differentiableOn h.1 h.2⟩

Premises used: WithTop.coe_le_coe._simp_1, contDiffOn_of_continuousOn_differentiableOn, ContDiffOn.continuousOn_iteratedFDerivWithin, cast, WithTop.coe_lt_coe._simp_1, And.right, And.left, And.intro, Iff.intro, Eq.symm, ContDiffOn.differentiableOn_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ 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

Tactic:
rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]

Premises used: contDiffOn_iff_continuousOn_differentiableOn, WithTop.coe_natCast
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ ((∀ (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:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
inr : ∀ (hn : n ≠ ∞), ContDiffOn 𝕜 (n + 1) f s
⊢ ContDiffOn 𝕜 (n + 1) f s

Tactic:
rcases eq_or_ne n ∞ with rfl | hn

Premises used: WithTop.some, eq_or_ne, Top.top, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
inl : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
⊢ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) f s

Tactic:
rw [ENat.coe_top_add_one, contDiffOn_infty]

Premises used: ENat.coe_top_add_one, contDiffOn_infty
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
apply : ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1) f s x
⊢ ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f s x

Tactic:
apply ContDiffWithinAt.of_le _ (show (m : ℕ∞ω) ≤ m + 1 from le_self_add)

Premises used: ContDiffWithinAt.of_le, le_self_add
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ Ne (α := ℕ∞ω) (↑m : ℕ∞ω) ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ ContDiffWithinAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑m : ℕ∞ω) 1) f s x

Tactic:
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp),
      insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem, contDiffWithinAt_succ_iff_hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ω → AnalyticOn 𝕜 f s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ ∃ 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:
exact ⟨s, self_mem_nhdsWithin, (by simp), fderivWithin 𝕜 f s,
      fun y hy => (hf y hy).hasFDerivWithinAt, (h x hx).of_le (mod_cast le_top)⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,
      insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem, contDiffWithinAt_succ_iff_hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ ∃ 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:
⟨s, self_mem_nhdsWithin, h', fderivWithin 𝕜 f s,
      fun y hy => (hf y hy).hasFDerivWithinAt, h x hx⟩

Premises used: fderivWithin, self_mem_nhdsWithin, And.intro, Exists.intro, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ ∃ 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:
exact ⟨s, self_mem_nhdsWithin, h', fderivWithin 𝕜 f s,
      fun y hy => (hf y hy).hasFDerivWithinAt, h x hx⟩