Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case left.he
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ e.symm ≫ₕ f ∈ contDiffGroupoid n I

pp: case left.he'
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ e'.symm ≫ₕ f' ∈ contDiffGroupoid n I'

pp: case right.he
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ f.symm ≫ₕ e ∈ contDiffGroupoid n I

pp: case right.he'
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ f'.symm ≫ₕ e' ∈ contDiffGroupoid n I'

Tactic:
<;>

Goal state after:
case left.he
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ e.symm ≫ₕ f ∈ contDiffGroupoid n I

case left.he'
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ e'.symm ≫ₕ f' ∈ contDiffGroupoid n I'

case right.he
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ f.symm ≫ₕ e ∈ contDiffGroupoid n I

case right.he'
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ f'.symm ≫ₕ e' ∈ contDiffGroupoid n I'