internlm/Lean-Github huggingface dataset:
Theorem: ofSet_in_maximal_atlas
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
s : Set E
hs : IsOpen s
e' : PartialHomeomorph E E
he' : e' ∈ atlas E E
⊢ (PartialHomeomorph.ofSet s hs).symm.trans e' ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
    e'.symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Tactic:
rw [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
s : Set E
hs : IsOpen s
e' : PartialHomeomorph E E
he' : e' ∈ atlas E E
⊢ (PartialHomeomorph.ofSet s hs).symm.trans (PartialHomeomorph.refl E) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
    (PartialHomeomorph.refl E).symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Theorem: ofSet_in_maximal_atlas
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
s : Set E
hs : IsOpen s
e' : PartialHomeomorph E E
he' : e' ∈ atlas E E
⊢ (PartialHomeomorph.ofSet s hs).symm.trans (PartialHomeomorph.refl E) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
    (PartialHomeomorph.refl E).symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Tactic:
simp only [mfld_simps]
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
s : Set E
hs : IsOpen s
e' : PartialHomeomorph E E
he' : e' ∈ atlas E E
⊢ PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Theorem: ofSet_in_maximal_atlas
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
s : Set E
hs : IsOpen s
e' : PartialHomeomorph E E
he' : e' ∈ atlas E E
⊢ PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Tactic:
apply ofSet_mem_contDiffGroupoid
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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
have : IsOpen ((e.extend I) '' e.source) := e.extend_isOpenMapOn_source I e.open_source (Eq.subset rfl)
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)
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(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)
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
let e' : PartialHomeomorph E E := PartialHomeomorph.ofSet (e.extend I '' e.source) this
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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
have h1 : e ∈ maximalAtlas I M := subset_maximalAtlas _ 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
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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
have h2 : e' ∈ maximalAtlas 𝓘(ℝ, E) E := ofSet_in_maximal_atlas this
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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(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
⊢ ContMDiffOn 𝓘(ℝ, E) I ⊤ (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
apply (contMDiffOn_iff_of_mem_maximalAtlas' h2 h1 (Eq.subset rfl) (e.mapsTo_extend_symm I)).mpr
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
⊢ ContDiffOn ℝ ⊤ (↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm) (↑(e'.extend 𝓘(ℝ, E)) '' 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
⊢ ContDiffOn ℝ ⊤ (↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm) (↑(e'.extend 𝓘(ℝ, E)) '' e'.source)
Tactic:
apply ContMDiffOn.contDiffOn
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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ (↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm)
    (↑(e'.extend 𝓘(ℝ, E)) '' 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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ (↑(e.extend I) ∘ ↑(e.extend I).symm ∘ ↑(e'.extend 𝓘(ℝ, E)).symm)
    (↑(e'.extend 𝓘(ℝ, E)) '' e'.source)
Tactic:
set f := e.extend I ∘ (e.extend I).symm ∘ (PartialEquiv.symm (PartialHomeomorph.extend e' 𝓘(ℝ, E)))
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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' 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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' e'.source)
Tactic:
have cong : ∀ x ∈ e.extend I '' e.source, f x = x := fun x hx ↦ e.extend_right_inv I hx
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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' 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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' e'.source)
Tactic:
have h : (e'.extend 𝓘(ℝ, E)) '' e'.source = e.extend I '' e.source := by
  simp only [e', mfld_simps, image_id']
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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' 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
⊢ ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, E) ⊤ f (↑(e'.extend 𝓘(ℝ, E)) '' e'.source)
Tactic:
have : ((e'.extend 𝓘(ℝ, E)) '' (e.extend I '' e.source)) = e.extend I '' e.source := by
  have : e'.source = e.extend I '' e.source := by rw [PartialHomeomorph.ofSet_source]
  exact this ▸ h
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 𝓘(ℝ, E)) '' e'.source)