α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝 x,
    ↑e x ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑(LocalHomeomorph.symm e) ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
rw [eventuallyEq_set, e.eventually_nhds _ hxe]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ (a : α),
    a ∈ e.source →
      (a ∈ s → a ∈ f ⁻¹' t) →
        (↑e a ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t))
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝 x,
    ↑e x ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
filter_upwards [e.open_source.mem_nhds hxe,
  mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : α
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ (a : α),
    a ∈ e.source →
      (a ∈ s → a ∈ f ⁻¹' t) →
        (↑e a ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t))
intro y hy hyu
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.35170
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : α
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and_iff, iff_self_and,
  e.left_inv hy, iff_true_intro hyu]