-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem contDiffWithinAt_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) {x : E} (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : E
hx : x ∈ ↑I '' (f'.symm ≫ₕ f).source
⊢ ↑I '' (f'.symm ≫ₕ f).source ∈ 𝓝[range ↑I] x

Tactic:
obtain ⟨z, hz, rfl⟩ := hx

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
z : H
hz : z ∈ (f'.symm ≫ₕ f).source
⊢ ↑I '' (f'.symm ≫ₕ f).source ∈ 𝓝[range ↑I] ↑I z

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
z : H
hz : z ∈ (f'.symm ≫ₕ f).source
⊢ ↑I '' (f'.symm ≫ₕ f).source ∈ 𝓝[range ↑I] ↑I z

Tactic:
exact I.image_mem_nhdsWithin ((PartialHomeomorph.open_source _).mem_nhds hz)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : E
hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source
⊢ ContDiffWithinAt 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) (range ↑I) x

Tactic:
apply (contDiffOn_extend_coord_change hf hf' x hx).mono_of_mem_nhdsWithin

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : E
hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source
⊢ ((f'.extend I).symm ≫ f.extend I).source ∈ 𝓝[range ↑I] x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : E
hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source
⊢ ((f'.extend I).symm ≫ f.extend I).source ∈ 𝓝[range ↑I] x

Tactic:
rw [extend_coord_change_source] at hx ⊢

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : E
hx : x ∈ ↑I '' (f'.symm ≫ₕ f).source
⊢ ↑I '' (f'.symm ≫ₕ f).source ∈ 𝓝[range ↑I] x