Theorem: PartialHomeomorph.mapsTo_extend_symm (Sard/ManifoldAux.lean)

State before:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
⊢ MapsTo (↑(e.extend I).symm) (↑(e.extend I) '' e.source) e.source
Tactic:
rintro x ⟨s, hs, rfl⟩
State after:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source

State before:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Tactic:
have : (e.extend I).symm (e.extend I s) = s := e.extend_left_inv _ hs
State after:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source

State before:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Tactic:
rw [this]
State after:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source

State before:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source
Tactic:
exact hs
State after:
no goals