𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
hx : x ∈ f.source
⊢ ↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extend f I) x)]
    ↑(ModelWithCorners.symm I) ⁻¹' f.target ∩ (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I)
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
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
rw [f.extend_target, inter_assoc, inter_comm (range I)]
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
hx : x ∈ f.source
⊢ ↑(ModelWithCorners.symm I) ⁻¹' f.target ∈ 𝓝 (↑(extend f I) x)
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
hx : x ∈ f.source
⊢ univ ∩ (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I) =ᶠ[𝓝 (↑(extend f I) x)]
    ↑(ModelWithCorners.symm I) ⁻¹' f.target ∩ (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I)
refine' (eventuallyEq_univ.mpr _).symm.inter EventuallyEq.rfl
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
hx : x ∈ f.source
⊢ ↑(ModelWithCorners.symm I) (↑(extend f I) x) ∈ f.target
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
hx : x ∈ f.source
⊢ ↑(ModelWithCorners.symm I) ⁻¹' f.target ∈ 𝓝 (↑(extend f I) x)
refine' I.continuousAt_symm.preimage_mem_nhds (f.open_target.mem_nhds _)
no goals
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.162184
M' : Type ?u.162187
H' : Type ?u.162190
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
hx : x ∈ f.source
⊢ ↑(ModelWithCorners.symm I) (↑(extend f I) x) ∈ f.target
simp_rw [f.extend_coe, Function.comp_apply, I.left_inv, f.mapsTo hx]