𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.131353
M' : Type ?u.131356
H' : Type ?u.131359
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
hs : s ⊆ f.source
⊢ ↑I '' (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' s) ⊆ ↑I '' (↑(LocalHomeomorph.symm f) ⁻¹' s)
𝕜 : Type u_4
E : Type u_3
M : Type u_1
H : Type u_2
E' : Type ?u.131353
M' : Type ?u.131356
H' : Type ?u.131359
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
hs : s ⊆ f.source
⊢ MapsTo (↑(extend f I)) s (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I)
rw [mapsTo', extend_coe, extend_coe_symm, preimage_comp, ← I.image_eq, image_comp,
  f.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.131353
M' : Type ?u.131356
H' : Type ?u.131359
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
hs : s ⊆ f.source
⊢ ↑I '' (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' s) ⊆ ↑I '' (↑(LocalHomeomorph.symm f) ⁻¹' s)
exact image_subset _ (inter_subset_right _ _)