Theorem: extendedChart_symm_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 𝓘(ℝ, 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)
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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)))
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)

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
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)

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']
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)

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
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)

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]
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)

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))
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
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']
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
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]
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

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
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
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]
State after:
no goals