Theorem: extendedChart_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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ Bijective ⇑(mfderiv I 𝓘(ℝ, E) (↑(e.extend I)) x)
Tactic:
refine diffeoOn_differential_bijective I 𝓘(ℝ, E) (Eq.le rfl) e.open_source ?_ hx (mapsTo_image (e.extend I) e.source) ?_ ?_ ?_ ?_ diff
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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ ∀ x ∈ e.source, ↑(e.extend I).symm (↑(e.extend I) 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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ ∀ y ∈ ↑(e.extend I) '' e.source, ↑(e.extend I) (↑(e.extend I).symm 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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ ContMDiffOn I 𝓘(ℝ, E) (↑1) (↑(e.extend I)) e.source