Theorem: ofSet_in_maximal_atlas (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
s : Set E
hs : IsOpen s
⊢ PartialHomeomorph.ofSet s hs ∈ maximalAtlas 𝓘(ℝ, E) E
Tactic:
rw [maximalAtlas, mem_maximalAtlas_iff]
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' ∈ atlas E E,
    (PartialHomeomorph.ofSet s hs).symm.trans e' ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
      e'.symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)

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' ∈ atlas E E,
    (PartialHomeomorph.ofSet s hs).symm.trans e' ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
      e'.symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Tactic:
intro e' 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
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)

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

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

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