𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.164976
M' : Type ?u.164979
H' : Type ?u.164982
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 s : Set M
x : M
hs : s ⊆ (extend f I).source
hx : x ∈ f.source
⊢ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extend f I) x)] ↑(extend f I) '' s
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.164976
M' : Type ?u.164979
H' : Type ?u.164982
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 s : Set M
x : M
hs : s ⊆ f.source
hx : x ∈ f.source
⊢ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extend f I) x)] ↑(extend f I) '' s
rw [← f.extend_source I] at hs
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.164976
M' : Type ?u.164979
H' : Type ?u.164982
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 s : Set M
x : M
hs : s ⊆ (extend f I).source
hx : x ∈ f.source
⊢ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extend f I) x)]
    (extend f I).target ∩ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.164976
M' : Type ?u.164979
H' : Type ?u.164982
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 s : Set M
x : M
hs : s ⊆ (extend f I).source
hx : x ∈ f.source
⊢ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extend f I) x)] ↑(extend f I) '' s
rw [(f.extend I).image_eq_target_inter_inv_preimage hs]
no goals
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.164976
M' : Type ?u.164979
H' : Type ?u.164982
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 s : Set M
x : M
hs : s ⊆ (extend f I).source
hx : x ∈ f.source
⊢ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extend f I) x)]
    (extend f I).target ∩ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s
exact f.extend_symm_preimage_inter_range_eventuallyEq_aux I hx