Theorem: extChartAt_symm_map_nhds' (Ray/AnalyticManifold/AnalyticManifold.lean)

State before:
𝕜 : Type
inst✝²⁹ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁸ : NormedAddCommGroup E
inst✝²⁷ : NormedSpace 𝕜 E
inst✝²⁶ : CompleteSpace E
inst✝²⁵ : TopologicalSpace A
F B : Type
inst✝²⁴ : NormedAddCommGroup F
inst✝²³ : NormedSpace 𝕜 F
inst✝²² : CompleteSpace F
inst✝²¹ : TopologicalSpace B
G C : Type
inst✝²⁰ : NormedAddCommGroup G
inst✝¹⁹ : NormedSpace 𝕜 G
inst✝¹⁸ : TopologicalSpace C
H D : Type
inst✝¹⁷ : NormedAddCommGroup H
inst✝¹⁶ : NormedSpace 𝕜 H
inst✝¹⁵ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹⁴ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹³ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹² : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹¹ : TopologicalSpace P
inst✝¹⁰ : I✝.Boundaryless
inst✝⁹ : ChartedSpace A M✝
cm : AnalyticManifold I✝ M✝
inst✝⁸ : J.Boundaryless
inst✝⁷ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁶ : K.Boundaryless
inst✝⁵ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁴ : L.Boundaryless
inst✝³ : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝² : I.Boundaryless
M : Type
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
x : M
⊢ Filter.map (↑(extChartAt I x).symm) (𝓝 (↑(extChartAt I x) x)) = 𝓝 x
Tactic:
convert extChartAt_symm_map_nhds (mem_extChartAt_target I x)
State after:
case h.e'_3.h.e'_3
𝕜 : Type
inst✝²⁹ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁸ : NormedAddCommGroup E
inst✝²⁷ : NormedSpace 𝕜 E
inst✝²⁶ : CompleteSpace E
inst✝²⁵ : TopologicalSpace A
F B : Type
inst✝²⁴ : NormedAddCommGroup F
inst✝²³ : NormedSpace 𝕜 F
inst✝²² : CompleteSpace F
inst✝²¹ : TopologicalSpace B
G C : Type
inst✝²⁰ : NormedAddCommGroup G
inst✝¹⁹ : NormedSpace 𝕜 G
inst✝¹⁸ : TopologicalSpace C
H D : Type
inst✝¹⁷ : NormedAddCommGroup H
inst✝¹⁶ : NormedSpace 𝕜 H
inst✝¹⁵ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹⁴ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹³ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹² : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹¹ : TopologicalSpace P
inst✝¹⁰ : I✝.Boundaryless
inst✝⁹ : ChartedSpace A M✝
cm : AnalyticManifold I✝ M✝
inst✝⁸ : J.Boundaryless
inst✝⁷ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁶ : K.Boundaryless
inst✝⁵ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁴ : L.Boundaryless
inst✝³ : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝² : I.Boundaryless
M : Type
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
x : M
⊢ x = ↑(extChartAt I x).symm (↑(extChartAt I x) x)

State before:
case h.e'_3.h.e'_3
𝕜 : Type
inst✝²⁹ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁸ : NormedAddCommGroup E
inst✝²⁷ : NormedSpace 𝕜 E
inst✝²⁶ : CompleteSpace E
inst✝²⁵ : TopologicalSpace A
F B : Type
inst✝²⁴ : NormedAddCommGroup F
inst✝²³ : NormedSpace 𝕜 F
inst✝²² : CompleteSpace F
inst✝²¹ : TopologicalSpace B
G C : Type
inst✝²⁰ : NormedAddCommGroup G
inst✝¹⁹ : NormedSpace 𝕜 G
inst✝¹⁸ : TopologicalSpace C
H D : Type
inst✝¹⁷ : NormedAddCommGroup H
inst✝¹⁶ : NormedSpace 𝕜 H
inst✝¹⁵ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹⁴ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹³ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹² : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹¹ : TopologicalSpace P
inst✝¹⁰ : I✝.Boundaryless
inst✝⁹ : ChartedSpace A M✝
cm : AnalyticManifold I✝ M✝
inst✝⁸ : J.Boundaryless
inst✝⁷ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁶ : K.Boundaryless
inst✝⁵ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁴ : L.Boundaryless
inst✝³ : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝² : I.Boundaryless
M : Type
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
x : M
⊢ x = ↑(extChartAt I x).symm (↑(extChartAt I x) x)
Tactic:
simp only [PartialEquiv.left_inv _ (mem_extChartAt_source I x)]
State after:
no goals