-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_symm_preimage_inter_range_eventuallyEq_aux {s : Set M} {x : M} (hx : x ∈ f.source) :
    ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)]
      ((f.extend I).target ∩ (f.extend I).symm ⁻¹' s : Set _)

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ ↑I.symm ⁻¹' f.target ∈ 𝓝 (↑(f.extend I) x)

Tactic:
refine I.continuousAt_symm.preimage_mem_nhds (f.open_target.mem_nhds ?_)

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ ↑I.symm (↑(f.extend I) x) ∈ f.target

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ ↑(f.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] (f.extend I).target ∩ ↑(f.extend I).symm ⁻¹' s

Tactic:
rw [f.extend_target, inter_assoc, inter_comm (range I)]

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ ↑(f.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(f.extend I) x)]
    ↑I.symm ⁻¹' f.target ∩ (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ ↑I.symm (↑(f.extend I) x) ∈ f.target

Tactic:
simp_rw [f.extend_coe, Function.comp_apply, I.left_inv, f.mapsTo hx]

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ univ ∩ (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) =ᶠ[𝓝 (↑(f.extend I) x)]
    ↑I.symm ⁻¹' f.target ∩ (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)

Tactic:
refine (eventuallyEq_univ.mpr ?_).symm.inter EventuallyEq.rfl

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hx : x ∈ f.source
⊢ ↑I.symm ⁻¹' f.target ∈ 𝓝 (↑(f.extend I) x)