case intro
α : Type u_1
β : Type u_2
γ : Type ?u.106516
δ : Type ?u.106519
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ 𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source
α : Type u_1
β : Type u_2
γ : Type ?u.106516
δ : Type ?u.106519
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source
lift x to e.source using hx
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.106516
δ : Type ?u.106519
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (↑(toHomeomorphSourceTarget e)) (comap Subtype.val (𝓝 ↑(↑(toHomeomorphSourceTarget e) x)))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.106516
δ : Type ?u.106519
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ 𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source
rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
  e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]