-- Mathlib/Topology/PartialHomeomorph.lean
theorem preimage_eventuallyEq_target_inter_preimage_inter {e : PartialHomeomorph X Y} {s : Set X}
    {t : Set Z} {x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source)
    (ht : t ∈ 𝓝 (f x)) :
    e.symm ⁻¹' s =ᶠ[𝓝 (e x)] (e.target ∩ e.symm ⁻¹' (s ∩ f ⁻¹' t) : Set Y)

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
rw [eventuallyEq_set, e.eventually_nhds _ hxe]

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : X) in 𝓝 x, ↑e x ∈ ↑e.symm ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Proof state:
case h
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ a ∈ e.source, (a ∈ s → a ∈ f ⁻¹' t) → (↑e a ∈ ↑e.symm ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t))

Tactic:
intro y hy hyu

Result:
case h
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Proof state:
case h
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and, iff_self_and,
  e.left_inv hy, iff_true_intro hyu]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : X) in 𝓝 x, ↑e x ∈ ↑e.symm ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
filter_upwards [e.open_source.mem_nhds hxe,
  mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]

Result:
case h
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ a ∈ e.source, (a ∈ s → a ∈ f ⁻¹' t) → (↑e a ∈ ↑e.symm ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t))