-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffAt_iff_contMDiffAt_nhds
    [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
    ContMDiffAt I I' n f x ↔ ∀ᶠ x' in 𝓝 x, ContMDiffAt I I' n f x'

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffAt I I' n f x → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
rw [contMDiffAt_iff_contMDiffOn_nhds hn]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ (∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u) → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ (∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u) → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
rintro ⟨u, hu, h⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
x' : M
hx' : u ∈ 𝓝 x'
⊢ ContMDiffAt I I' n f x'

Tactic:
exact (h x' <| mem_of_mem_nhds hx').contMDiffAt hx'

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffAt I I' n f x ↔ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
refine ⟨?_, fun h => h.self_of_nhds⟩

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffAt I I' n f x → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
refine (eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_

Result:
case intro.intro
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
x' : M
hx' : u ∈ 𝓝 x'
⊢ ContMDiffAt I I' n f x'