Theorem: extendedChart_symm_differential_bijective
Proof 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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ Bijective ⇑(mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x)
Tactic:
refine diffeoOn_differential_bijective 𝓘(ℝ, E) I (Eq.le rfl) ?_ e.open_source hx ?_ (mapsTo_image (e.extend I) e.source) ?_ ?_ ?_ ?_
Proof state after:
case refine_1
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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ IsOpen (↑(e.extend I) '' e.source)

case refine_2
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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ MapsTo (↑(e.extend I).symm) (↑(e.extend I) '' e.source) e.source

case refine_3
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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ ∀ x ∈ ↑(e.extend I) '' e.source, ↑(e.extend I) (↑(e.extend I).symm x) = x

case refine_4
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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ ∀ y ∈ e.source, ↑(e.extend I).symm (↑(e.extend I) y) = y

case refine_5
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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ ContMDiffOn 𝓘(ℝ, E) I (↑1) (↑(e.extend I).symm) (↑(e.extend I) '' e.source)

case refine_6
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
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : E
hx : x ∈ ↑(e.extend I) '' e.source
⊢ ContMDiffOn I 𝓘(ℝ, E) (↑1) (↑(e.extend I)) e.source