𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.150056
M' : Type ?u.150059
H' : Type ?u.150062
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
y : M
hy : y ∈ f.source
e : LocalEquiv M E := extend f I
⊢ map (↑e) (𝓝[s] y) = 𝓝[↑e '' (e.source ∩ s)] ↑e y
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.150056
M' : Type ?u.150059
H' : Type ?u.150062
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
y : M
hy : y ∈ f.source
⊢ map (↑(extend f I)) (𝓝[s] y) = 𝓝[↑(extend f I) '' ((extend f I).source ∩ s)] ↑(extend f I) y
set e := f.extend I
no goals
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.150056
M' : Type ?u.150059
H' : Type ?u.150062
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
y : M
hy : y ∈ f.source
e : LocalEquiv M E := extend f I
⊢ map (↑e) (𝓝[s] y) = 𝓝[↑e '' (e.source ∩ s)] ↑e y
calc
  map e (𝓝[s] y) = map e (𝓝[e.source ∩ s] y) :=
    congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f I hy)).symm
  _ = 𝓝[e '' (e.source ∩ s)] e y :=
    ((f.extend I).leftInvOn.mono <| inter_subset_left _ _).map_nhdsWithin_eq
      ((f.extend I).left_inv <| by rwa [f.extend_source])
      (continuousAt_extend_symm f I hy).continuousWithinAt
      (continuousAt_extend f I hy).continuousWithinAt
no goals
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.150056
M' : Type ?u.150059
H' : Type ?u.150062
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
y : M
hy : y ∈ f.source
e : LocalEquiv M E := extend f I
⊢ y ∈ (extend f I).source
rwa [f.extend_source]