Theorem: extendedChart_smooth (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
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
let e' : PartialHomeomorph E E := PartialHomeomorph.refl E
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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
have h₁ : e ∈ maximalAtlas I M := subset_maximalAtlas _ he
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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
have h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E := subset_maximalAtlas _ (by rfl)
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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
set f := e.extend I ∘ (e.extend I).symm
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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
have h : ∀ x ∈ (e.extend I) '' e.source, f x = x := fun _ hx ↦ e.extend_right_inv I hx
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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
apply (contMDiffOn_iff_of_mem_maximalAtlas' h₁ h₂ (Eq.subset rfl) (mapsTo_univ _ _)).mpr
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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContDiffOn ℝ ⊤ (↑(e'.extend 𝓘(ℝ, E)) ∘ ↑(e.extend I) ∘ ↑(e.extend I).symm) (↑(e.extend I) '' e.source)

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContDiffOn ℝ ⊤ (↑(e'.extend 𝓘(ℝ, E)) ∘ ↑(e.extend I) ∘ ↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
exact ContMDiffOn.contDiffOn (fun x hx ↦ ContMDiffWithinAt.congr smoothWithinAt_id h (h x hx))
State after:
no goals

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
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
⊢ e' ∈ atlas E E
Tactic:
rfl
State after:
no goals