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
h : ContDiffOn 𝕜 ω f s
⊢ AnalyticOn 𝕜 f s

Tactic:
fun x hx ↦ (h x hx).analyticWithinAt

Premises used: AnalyticOn, 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
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.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
x : E
n : ℕ∞ω
hn : n ≠ ∞
refine_1 : ∀ (h : ContDiffWithinAt 𝕜 n f s x), ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
refine_2 : ∀ (h : ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u), ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffWithinAt 𝕜 n f s x
⊢ n = ∞ → n = ω

Tactic:
simp [hn]
-- 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffWithinAt 𝕜 n f s x
refine_1 :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (h'u : u ⊆ insert x s ∧ ContDiffOn 𝕜 n f u),
    ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
⊢ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

Tactic:
rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, h'u⟩

Premises used: le_rfl, 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
h'u : u ⊆ insert x s ∧ ContDiffOn 𝕜 n f u
⊢ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

Tactic:
⟨u, hu, h'u.2⟩

Premises used: And.right, And.intro, Exists.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
x : E
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
h'u : u ⊆ insert x s ∧ ContDiffOn 𝕜 n f u
⊢ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u

Tactic:
exact ⟨u, hu, h'u.2⟩
-- 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 : ℕ∞ω
hn : n ≠ ∞
h : ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u
refine_2 : ∀ (u : Set E) (u_mem : u ∈ 𝓝[insert x s] x) (hu : ContDiffOn 𝕜 n f u), ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
rcases h with ⟨u, u_mem, hu⟩
-- 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 : ℕ∞ω
hn : n ≠ ∞
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
hu : ContDiffOn 𝕜 n f u
⊢ x ∈ u

Tactic:
have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert x s) u_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
x : E
n : ℕ∞ω
hn : n ≠ ∞
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
hu : ContDiffOn 𝕜 n f u
this : x ∈ u
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
(hu x this).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert x s) u_mem)

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Set.subset_insert, nhdsWithin_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 : ℕ∞ω
hn : n ≠ ∞
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
hu : ContDiffOn 𝕜 n f u
this : x ∈ u
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
exact (hu x this).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert x s) u_mem)

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Set.subset_insert, nhdsWithin_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
hn : n ≠ ∞
⊢ n = ∞ → n = ω

Tactic:
simp [hn]
-- 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
hn : n ≠ ∞
rcases :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x),
    u ⊆ insert x s → ∀ (hd : ContDiffOn 𝕜 n f u), ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y

Tactic:
rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, _, hd⟩

Premises used: le_rfl, 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 : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u

Tactic:
have : ∀ᶠ y : E in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u :=
    (eventually_eventually_nhdsWithin.2 hu).and hu
-- 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
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
this : ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y

Tactic:
this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Filter.Eventually.mono, And.right
-- 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
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
this : ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u
refine : ∀ (y : E) (hy : u ∈ 𝓝[insert x s] y ∧ y ∈ u), u ∈ 𝓝[s] y
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y

Tactic:
refine this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Filter.Eventually.mono, And.right
-- 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
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
this : ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u
y : E
hy : u ∈ 𝓝[insert x s] y ∧ y ∈ u
⊢ u ∈ 𝓝[s] y

Tactic:
nhdsWithin_mono y (subset_insert _ _) hy.1

Premises used: And.left, Set.subset_insert, nhdsWithin_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
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
left : u ⊆ insert x s
hd : ContDiffOn 𝕜 n f u
this : ∀ᶠ (y : E) in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u
y : E
hy : u ∈ 𝓝[insert x s] y ∧ y ∈ u
⊢ u ∈ 𝓝[s] y

Tactic:
exact nhdsWithin_mono y (subset_insert _ _) hy.1

Premises used: And.left, Set.subset_insert, nhdsWithin_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
n : ℕ∞ω
h : ContDiffOn 𝕜 (n + 1) f s
⊢ ContDiffOn 𝕜 n f s

Tactic:
h.of_le le_self_add

Premises used: ContDiffOn.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
n : ℕ∞ω
h : ContDiffOn 𝕜 (n + 1) f s
⊢ ContDiffOn 𝕜 1 f s

Tactic:
h.of_le le_add_self

Premises used: ContDiffOn.of_le, le_add_self
-- 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 : ℕ∞
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiffOn 𝕜 (↑m : ℕ∞ω) f s

Tactic:
⟨fun H _ hm => H.of_le (mod_cast hm), fun H x hx m hm => H m hm x hx m le_rfl⟩

Premises used: le_rfl, WithTop.coe_le_coe._simp_1, cast, ContDiffOn.of_le, Iff.intro, 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
⊢ (∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) ⊤ → ContDiffOn 𝕜 (↑m : ℕ∞ω) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
simp only [le_top, forall_prop_of_true]

Premises used: le_top, forall_prop_of_true
-- 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 : ℕ∞), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
⟨fun H n => H n, ?_⟩

Premises used: Nat.cast, Iff.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
refine : (∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s) → ∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
⊢ (∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
refine ⟨fun H n => H n, ?_⟩
-- 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
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
⊢ ContDiffOn 𝕜 (↑none : ℕ∞ω) f s

Tactic:
contDiffOn_infty.2 H

Premises used: Iff.mpr, 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
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
n : ℕ
⊢ ContDiffOn 𝕜 (↑(some n) : ℕ∞ω) f s

Tactic:
H n

Premises used: WithTop.some
-- 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
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
⊢ ContDiffOn 𝕜 (↑none : ℕ∞ω) f s

Tactic:
exacts [contDiffOn_infty.2 H, H n]

Premises used: Iff.mpr, 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
⊢ ContinuousOn f s

Tactic:
fun x hx =>
  (h x hx).continuousWithinAt

Premises used: ContDiffWithinAt.continuousWithinAt, ContinuousOn
-- 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
h : ContDiffOn 𝕜 0 f s
⊢ ContinuousOn f s

Tactic:
fun x hx =>
  (h x hx).continuousWithinAt

Premises used: ContDiffWithinAt.continuousWithinAt, ContinuousOn
-- 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 f₁ : E → F
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
h₁ : ∀ x ∈ s, f₁ x = f x
⊢ ContDiffOn 𝕜 n f₁ s

Tactic:
fun x hx => (h x hx).congr h₁ (h₁ x hx)

Premises used: ContDiffOn, ContDiffWithinAt.congr
-- 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 f₁ : E → F
n : ℕ∞ω
h₁ : ∀ x ∈ s, f₁ x = f x
⊢ ContDiffOn 𝕜 n f₁ s ↔ ContDiffOn 𝕜 n f s

Tactic:
⟨fun H => H.congr fun x hx => (h₁ x hx).symm, fun H => H.congr h₁⟩

Premises used: ContDiffOn.congr, Iff.intro, 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
t : Set E
hst : t ⊆ s
⊢ ContDiffOn 𝕜 n f t

Tactic:
fun x hx => (h x (hst hx)).mono hst

Premises used: ContDiffOn, 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 s₁ : Set E
f f₁ : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
h₁ : ∀ x ∈ s₁, f₁ x = f x
hs : s₁ ⊆ s
⊢ ContDiffOn 𝕜 n f₁ s₁

Tactic:
(hf.mono hs).congr h₁

Premises used: ContDiffOn.congr, ContDiffOn.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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hn : n ≠ 0
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun x hx => (h x hx).differentiableWithinAt hn

Premises used: DifferentiableOn, 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
s : Set E
f : E → F
h : ContDiffOn 𝕜 1 f s
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun x hx => (h x hx).differentiableWithinAt one_ne_zero

Premises used: DifferentiableOn, one_ne_zero, 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
s : Set E
f : E → F
n : ℕ∞ω
h :
  ∀ x ∈ s,
    ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
rcases :
  ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
    (hu : ContDiffOn 𝕜 n f (s ∩ u)), ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
rcases h x xs with ⟨u, u_open, xu, hu⟩
-- 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 :
  ∀ x ∈ s,
    ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
apply : u ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
apply (contDiffWithinAt_inter _).1 (hu x ⟨xs, xu⟩)

Premises used: And.intro, Iff.mp, 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 : ℕ∞ω
h :
  ∀ x ∈ s,
    ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ u ∈ 𝓝 x

Tactic:
IsOpen.mem_nhds u_open xu

Premises used: 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
n : ℕ∞ω
h :
  ∀ x ∈ s,
    ∃ (u : Set E), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ u ∈ 𝓝 x

Tactic:
exact IsOpen.mem_nhds u_open xu

Premises used: 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
n : ℕ∞ω
hn : n ≠ ∞
mp :
  ContDiffOn 𝕜 (n + 1) f s →
    ∀ x ∈ s,
      ∃ u ∈ 𝓝[insert x s] x,
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
mpr :
  (∀ x ∈ s,
      ∃ u ∈ 𝓝[insert x s] x,
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u) →
    ContDiffOn 𝕜 (n + 1) f s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    ∀ x ∈ s,
      ∃ u ∈ 𝓝[insert x s] x,
        (n = ω → AnalyticOn 𝕜 f u) ∧
          ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
constructor
-- 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
mp :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (f_an : n = ω → AnalyticOn 𝕜 f u) (f' : E → E →L[𝕜] F)
    (hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) (Hf' : ContDiffWithinAt 𝕜 n f' u x),
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).1 (h x hx) with
      ⟨u, hu, f_an, f', hf', Hf'⟩

Premises used: Iff.mp, 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ n = ∞ → n = ω

Tactic:
simp [hn]
-- 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
mp :
  ∀ (v : Set E) (vu : v ∈ 𝓝[insert x u] x) (v'u : v ⊆ insert x u) (hv : ContDiffOn 𝕜 n f' v),
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
rcases Hf'.contDiffOn le_rfl (by simp [hn]) with ⟨v, vu, v'u, hv⟩

Premises used: le_rfl, 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
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
mp :
  ∀ (hu : u ∈ 𝓝[s] x) (f_an : n = ω → AnalyticOn 𝕜 f u) (f' : E → E →L[𝕜] F)
    (hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) (Hf' : ContDiffWithinAt 𝕜 n f' u x) (v : Set E)
    (vu : v ∈ 𝓝[insert x u] x) (v'u : v ⊆ insert x u) (hv : ContDiffOn 𝕜 n f' v),
    ∃ u ∈ 𝓝[s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧
        ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ (f' : E → E →L[𝕜] F), (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
rw [insert_eq_of_mem hx] at hu ⊢

Premises used: Set.insert_eq_of_mem