no goals
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : H
s : Set H
⊢ map (↑(ModelWithCorners.symm I)) (𝓝[↑I '' s] ↑I x) = 𝓝[s] x
rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]