Theorem: extendedChart_symm_differential_bijective (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
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) ?_ ?_ ?_ ?_
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

State before:
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)
Tactic:
exact e.extend_isOpenMapOn_source I e.open_source (Eq.subset rfl)
State after:
no goals

State before:
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
Tactic:
rintro x ⟨s, hs, rfl⟩
State after:
case refine_2.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
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
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source

State before:
case refine_2.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
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
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 refine_2.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
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
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 refine_2.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
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
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 refine_2.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
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
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source

State before:
case refine_2.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
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
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

State before:
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
Tactic:
exact fun x hx ↦ e.extend_right_inv _ hx
State after:
no goals

State before:
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
Tactic:
exact fun x hx ↦ e.extend_left_inv _ hx
State after:
no goals

State before:
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)
Tactic:
exact SmoothOn.contMDiffOn (extendedChart_symm_smooth I he)
State after:
no goals

State before:
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
Tactic:
exact SmoothOn.contMDiffOn (extendedChart_smooth I he)
State after:
no goals