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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
h_1 : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
h : ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
rcases :
  ∀ (f' : E → E →L[𝕜] F) (h1 : ContDiffOn 𝕜 n f' s) (h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x),
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s

Tactic:
rcases h with ⟨f', h1, h2⟩
-- 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
h : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
f' : E → E →L[𝕜] F
h1 : ContDiffOn 𝕜 n f' s
h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s

Tactic:
⟨fun x hx => (h2 x hx).differentiableWithinAt, f_an, fun x hx => ?_⟩

Premises used: HasFDerivWithinAt.differentiableWithinAt, And.intro
-- 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
h : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
f' : E → E →L[𝕜] F
h1 : ContDiffOn 𝕜 n f' s
h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
refine : ∀ (x : E) (hx : x ∈ s), ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s x
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s

Tactic:
refine ⟨fun x hx => (h2 x hx).differentiableWithinAt, f_an, fun x hx => ?_⟩
-- 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
h : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
f' : E → E →L[𝕜] F
h1 : ContDiffOn 𝕜 n f' s
h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s x

Tactic:
(h1 x hx).congr_of_mem (fun y hy => (h2 y hy).fderivWithin (hs y hy)) hx

Premises used: HasFDerivWithinAt.fderivWithin, ContDiffWithinAt.congr_of_mem
-- 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
h : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
f' : E → E →L[𝕜] F
h1 : ContDiffOn 𝕜 n f' s
h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s x

Tactic:
exact (h1 x hx).congr_of_mem (fun y hy => (h2 y hy).fderivWithin (hs y hy)) hx

Premises used: HasFDerivWithinAt.fderivWithin, ContDiffWithinAt.congr_of_mem
-- 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
hs : UniqueDiffOn 𝕜 s
rw :
  DifferentiableOn 𝕜 f s ∧
      (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderivWithin 𝕜 f s) s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderivWithin 𝕜 f s) s

Tactic:
rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin hs]

Premises used: ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin
-- 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
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧
      (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderivWithin 𝕜 f s) s

Tactic:
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 : ℕ∞ω
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw :
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
rw₁ rw₂ :
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fun (x : E) ↦ fderiv 𝕜 f x) s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f) s

Tactic:
rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
    contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]

Premises used: contDiffOn_congr, fderivWithin_of_isOpen, contDiffOn_succ_iff_fderivWithin, IsOpen.uniqueDiffOn
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw :
  DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderiv 𝕜 f) s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f) s

Tactic:
rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]

Premises used: ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderiv 𝕜 f) s

Tactic:
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
m n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 (F := E →L[𝕜] F) m (fderivWithin 𝕜 f s) s

Tactic:
((contDiffOn_succ_iff_fderivWithin hs).1 (hf.of_le hmn)).2.2

Premises used: ContDiffOn.of_le, And.right, contDiffOn_succ_iff_fderivWithin, Iff.mp
-- 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
m n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 (F := E →L[𝕜] F) m (fderiv 𝕜 f) s

Tactic:
(hf.fderivWithin hs.uniqueDiffOn hmn).congr fun _ hx => (fderivWithin_of_isOpen hs hx).symm

Premises used: ContDiffOn.congr, fderivWithin_of_isOpen, ContDiffOn.fderivWithin, IsOpen.uniqueDiffOn, Eq.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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 1 ≤ n
⊢ ContinuousOn (Y := E →L[𝕜] F) (fderivWithin 𝕜 f s) s

Tactic:
((contDiffOn_succ_iff_fderivWithin hs).1
    (h.of_le (show 0 + (1 : ℕ∞ω) ≤ n from hn))).2.2.continuousOn

Premises used: ContDiffOn.of_le, And.right, ContDiffOn.continuousOn, contDiffOn_succ_iff_fderivWithin, Iff.mp
-- 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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hn : 1 ≤ n
⊢ ContinuousOn (Y := E →L[𝕜] F) (fderiv 𝕜 f) s

Tactic:
((contDiffOn_succ_iff_fderiv_of_isOpen hs).1
    (h.of_le (show 0 + (1 : ℕ∞ω) ≤ n from hn))).2.2.continuousOn

Premises used: contDiffOn_succ_iff_fderiv_of_isOpen, ContDiffOn.of_le, And.right, ContDiffOn.continuousOn, Iff.mp
-- 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
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x

Tactic:
Iff.rfl

Premises used: ContDiffAt, Iff.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
f : E → F
x : E
⊢ ContDiffAt 𝕜 ∞ f x ↔ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n : ℕ∞ω) f x

Tactic:
simp [← contDiffWithinAt_univ, contDiffWithinAt_infty]

Premises used: contDiffWithinAt_univ, contDiffWithinAt_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
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
h.mono (subset_univ _)

Premises used: Set.subset_univ, ContDiffWithinAt.mono
-- 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 : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
rwa : ContDiffWithinAt 𝕜 n f univ x
rwa₁ : ContDiffWithinAt 𝕜 n f (univ ∩ s) x
rwa₂ rwa₃ rwa₄ rwa₅ : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffAt 𝕜 n f x

Tactic:
rwa [ContDiffAt, ← contDiffWithinAt_inter hx, univ_inter]

Premises used: ContDiffAt, Set.univ_inter, contDiffWithinAt_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 : ℕ∞ω
h : s ∈ 𝓝 x
rw : ContDiffWithinAt 𝕜 n f (univ ∩ s) x ↔ ContDiffAt 𝕜 n f x
rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
rw₂ rw₃ : ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_univ]

Premises used: contDiffWithinAt_univ, Set.univ_inter, contDiffWithinAt_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
n : ℕ∞ω
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContDiffOn 𝕜 n f s ↔ ∀ ⦃a : E⦄, a ∈ s → ContDiffAt 𝕜 n f a

Tactic:
forall₂_congr fun _ => contDiffWithinAt_iff_contDiffAt ∘ hs.mem_nhds

Premises used: ContDiffOn, Function.comp, contDiffWithinAt_iff_contDiffAt, forall₂_congr, 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 : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hx : s ∈ 𝓝 x
⊢ ContDiffAt 𝕜 n f x

Tactic:
(h _ (mem_of_mem_nhds hx)).contDiffAt hx

Premises used: ContDiffWithinAt.contDiffAt, mem_of_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
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
hg rwa rwa₁ rwa₂ rwa₃ : f₁ =ᶠ[𝓝 x] f
⊢ f₁ =ᶠ[𝓝[univ] x] f

Tactic:
rwa [nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- 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
f : E → F
x : E
m n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
hmn : m ≤ n
⊢ ContDiffAt 𝕜 m f x

Tactic:
ContDiffWithinAt.of_le h hmn

Premises used: ContDiffAt, ContDiffWithinAt.of_le
-- 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
f : E → F
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
⊢ ContinuousAt f x

Tactic:
simpa [continuousWithinAt_univ] using h.continuousWithinAt

Premises used: continuousWithinAt_univ, ContDiffWithinAt.continuousWithinAt
-- 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
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
⊢ ContDiffWithinAt 𝕜 ω f univ x

Tactic:
rw [← contDiffWithinAt_univ] at h

Premises used: contDiffWithinAt_univ
-- 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
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
rw : AnalyticWithinAt 𝕜 f univ x
⊢ AnalyticAt 𝕜 f x

Tactic:
rw [← analyticWithinAt_univ]

Premises used: analyticWithinAt_univ
-- 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
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticWithinAt 𝕜 f univ x

Tactic:
h.analyticWithinAt

Premises used: ContDiffWithinAt.analyticWithinAt
-- 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
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticWithinAt 𝕜 f univ x

Tactic:
exact h.analyticWithinAt

Premises used: ContDiffWithinAt.analyticWithinAt
-- 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
f : E → F
x : E
n : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticWithinAt 𝕜 f univ x

Tactic:
rw [← analyticWithinAt_univ] at h

Premises used: analyticWithinAt_univ
-- 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
f : E → F
x : E
n : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticWithinAt 𝕜 f univ x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
h.contDiffWithinAt

Premises used: AnalyticWithinAt.contDiffWithinAt
-- 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
f : E → F
x : E
n : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticWithinAt 𝕜 f univ x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
exact h.contDiffWithinAt

Premises used: AnalyticWithinAt.contDiffWithinAt
-- 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
f : E → F
x : E
n : ℕ∞ω
rw : ContDiffWithinAt 𝕜 n f (univ \ {x}) x ↔ ContDiffAt 𝕜 n f x
rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
rw₂ rw₃ : ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [compl_eq_univ_diff, contDiffWithinAt_diff_singleton, contDiffWithinAt_univ]

Premises used: contDiffWithinAt_univ, Set.compl_eq_univ_diff, contDiffWithinAt_diff_singleton
-- 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
f : E → F
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
hn : n ≠ 0
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa [hn, differentiableWithinAt_univ] using h.differentiableWithinAt

Premises used: differentiableWithinAt_univ, ContDiffWithinAt.differentiableWithinAt
-- 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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
rw :
  DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDeriv 𝕜 m f) univ x
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f) x

Tactic:
rw [← differentiableWithinAt_univ]

Premises used: differentiableWithinAt_univ
-- 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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
⊢ UniqueDiffOn 𝕜 (E := E) (insert x univ)

Tactic:
simp [uniqueDiffOn_univ]

Premises used: uniqueDiffOn_univ
-- 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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
h₁ :
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f)
    (iteratedFDerivWithin 𝕜 m f univ)
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDeriv 𝕜 m f) univ x

Tactic:
convert! (h.differentiableWithinAt_iteratedFDerivWithin hmn (by simp [uniqueDiffOn_univ]))

Premises used: ContDiffWithinAt.differentiableWithinAt_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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f)
    (iteratedFDerivWithin 𝕜 m f univ)

Tactic:
iteratedFDerivWithin_univ.symm

Premises used: Eq.symm, iteratedFDerivWithin_univ
-- 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
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : (↑m : ℕ∞ω) < n
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f)
    (iteratedFDerivWithin 𝕜 m f univ)

Tactic:
exact iteratedFDerivWithin_univ.symm

Premises used: Eq.symm, iteratedFDerivWithin_univ
-- 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
f : E → F
x : E
h : ContDiffAt 𝕜 1 f x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa [(le_refl 1), differentiableWithinAt_univ] using h.differentiableWithinAt

Premises used: le_refl, differentiableWithinAt_univ, OfNat.ofNat, ContDiffWithinAt.differentiableWithinAt
-- 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
f : E → F
x : E
m n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
hm : m ≤ n
h' : m = ∞ → n = ω
⊢ ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 m f u

Tactic:
simpa [nhdsWithin_univ] using h.contDiffOn hm h'

Premises used: nhdsWithin_univ, ContDiffAt.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
f : E → F
x : E
n : ℕ
⊢ Ne (α := ℕ∞ω) (↑n : ℕ∞ω) ∞

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
f : E → F
x : E
n : ℕ
rw :
  (∃ u ∈ 𝓝[insert x univ] x,
      (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f' u x) ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' x

Tactic:
rw [← contDiffWithinAt_univ, contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp)]

Premises used: contDiffWithinAt_univ, contDiffWithinAt_succ_iff_hasFDerivWithinAt