-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.eventually (h : ContDiffWithinAt 𝕜 n f s x) (hn : n ≠ ∞) :
    ∀ᶠ y in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
⊢ ∀ᶠ (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⟩

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
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, ContDiffWithinAt 𝕜 n f s y

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
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:
refine this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
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

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
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

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
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, ContDiffWithinAt 𝕜 n f s y

Tactic:
have : ∀ᶠ y : E in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u :=
  (eventually_eventually_nhdsWithin.2 hu).and hu

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
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

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
⊢ n = ∞ → n = ω

Tactic:
simp [hn]

Result:
no goals