internlm/Lean-Github huggingface dataset:
Theorem: extendedChart_symm_smooth
Proof state before:
case a
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this✝ : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this✝
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
this : ↑(e'.extend 𝓘(ℝ, E)) '' (↑(e.extend I) '' e.source) = ↑(e.extend I) '' e.source
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' e'.source)
Tactic:
rw [PartialHomeomorph.ofSet_source, this]
Proof state after:
case a
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this✝ : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this✝
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
this : ↑(e'.extend 𝓘(ℝ, E)) '' (↑(e.extend I) '' e.source) = ↑(e.extend I) '' e.source
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e.extend I) '' e.source)
Theorem: extendedChart_symm_smooth
Proof state before:
case a
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this✝ : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this✝
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
this : ↑(e'.extend 𝓘(ℝ, E)) '' (↑(e.extend I) '' e.source) = ↑(e.extend I) '' e.source
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e.extend I) '' e.source)
Tactic:
exact fun x hx ↦ ContMDiffWithinAt.congr smoothWithinAt_id cong (cong x (h ▸ hx))
Proof state after:
no goals
Theorem: extendedChart_symm_smooth
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
Tactic:
simp only [e', mfld_simps, image_id']
Proof state after:
no goals
Theorem: extendedChart_symm_smooth
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
⊢ ↑(e'.extend 𝓘(ℝ, E)) '' (↑(e.extend I) '' e.source) = ↑(e.extend I) '' e.source
Tactic:
have : e'.source = e.extend I '' e.source := by rw [PartialHomeomorph.ofSet_source]
Proof state after:
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this✝ : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this✝
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
this : e'.source = ↑(e.extend I) '' e.source
⊢ ↑(e'.extend 𝓘(ℝ, E)) '' (↑(e.extend I) '' e.source) = ↑(e.extend I) '' e.source
Theorem: extendedChart_symm_smooth
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this✝ : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this✝
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
this : e'.source = ↑(e.extend I) '' e.source
⊢ ↑(e'.extend 𝓘(ℝ, E)) '' (↑(e.extend I) '' e.source) = ↑(e.extend I) '' e.source
Tactic:
exact this ▸ h
Proof state after:
no goals
Theorem: extendedChart_symm_smooth
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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
this : IsOpen (↑(e.extend I) '' e.source)
e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (↑(e.extend I) '' e.source) this
h1 : e ∈ maximalAtlas I M
h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm
cong : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
h : ↑(e'.extend 𝓘(ℝ, E)) '' e'.source = ↑(e.extend I) '' e.source
⊢ e'.source = ↑(e.extend I) '' e.source
Tactic:
rw [PartialHomeomorph.ofSet_source]
Proof state after:
no goals
Theorem: extendedChart_symm_differential_bijective
Proof 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)
Proof state after:
no goals
Theorem: extendedChart_symm_differential_bijective
Proof 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⟩
Proof 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
Theorem: extendedChart_symm_differential_bijective
Proof 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
Proof 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
Theorem: extendedChart_symm_differential_bijective
Proof 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]
Proof 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
Theorem: extendedChart_symm_differential_bijective
Proof 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
Proof state after:
no goals
Theorem: extendedChart_symm_differential_bijective
Proof 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
Proof state after:
no goals
Theorem: extendedChart_symm_differential_bijective
Proof 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
Proof state after:
no goals
Theorem: extendedChart_symm_differential_bijective
Proof 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)
Proof state after:
no goals
Theorem: extendedChart_symm_differential_bijective
Proof 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)
Proof state after:
no goals
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
⊢ Bijective ⇑(mfderiv I 𝓘(ℝ, E) (↑(e.extend I)) x)
Tactic:
have diff : ContMDiffOn 𝓘(ℝ, E) I 1 (e.extend I).symm (e.extend I '' e.source) :=
  SmoothOn.contMDiffOn (extendedChart_symm_smooth I he)
Proof state after:
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)
Theorem: extendedChart_differential_bijective
Proof 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 : 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)
Tactic:
exact e.extend_isOpenMapOn_source I e.open_source (Eq.subset rfl)
Proof state after:
no goals
Theorem: extendedChart_differential_bijective
Proof 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 : 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
Tactic:
rintro x ⟨s, hs, rfl⟩
Proof 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 : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source