Theorem: AnalyticManifold.punctured_nhds_neBot (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
inst✝ : Nontrivial E
x : M
⊢ (𝓝[≠] x).NeBot
Tactic:
have p := Module.punctured_nhds_neBot 𝕜 E (extChartAt I x x)
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : (𝓝[≠] ↑(extChartAt I x) x).NeBot
⊢ (𝓝[≠] x).NeBot

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
inst✝ : Nontrivial E
x : M
p : (𝓝[≠] ↑(extChartAt I x) x).NeBot
⊢ (𝓝[≠] x).NeBot
Tactic:
simp only [← Filter.frequently_true_iff_neBot, frequently_nhdsWithin_iff, ←
  extChartAt_symm_map_nhds' I x, Filter.frequently_map, true_and_iff,
  mem_compl_singleton_iff] at p ⊢
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
⊢ ∃ᶠ (a : E) in 𝓝 (↑(extChartAt I x) x), ↑(extChartAt I x).symm a ≠ x

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
⊢ ∃ᶠ (a : E) in 𝓝 (↑(extChartAt I x) x), ↑(extChartAt I x).symm a ≠ x
Tactic:
apply p.mp
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
⊢ ∀ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x → ↑(extChartAt I x).symm x_1 ≠ x

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
⊢ ∀ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x → ↑(extChartAt I x).symm x_1 ≠ x
Tactic:
apply ((isOpen_extChartAt_target I x).eventually_mem (mem_extChartAt_target I x)).mp
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
⊢ ∀ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x),
    x_1 ∈ (extChartAt I x).target → x_1 ≠ ↑(extChartAt I x) x → ↑(extChartAt I x).symm x_1 ≠ x

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
⊢ ∀ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x),
    x_1 ∈ (extChartAt I x).target → x_1 ≠ ↑(extChartAt I x) x → ↑(extChartAt I x).symm x_1 ≠ x
Tactic:
refine eventually_of_forall fun y m h ↦ ?_
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : y ≠ ↑(extChartAt I x) x
⊢ ↑(extChartAt I x).symm y ≠ x

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : y ≠ ↑(extChartAt I x) x
⊢ ↑(extChartAt I x).symm y ≠ x
Tactic:
contrapose h
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ¬↑(extChartAt I x).symm y ≠ x
⊢ ¬y ≠ ↑(extChartAt I x) x

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ¬↑(extChartAt I x).symm y ≠ x
⊢ ¬y ≠ ↑(extChartAt I x) x
Tactic:
simp only [not_not] at m h ⊢
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) x

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) x
Tactic:
nth_rw 2 [← h]
State after:
𝕜 : 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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) (↑(extChartAt I x).symm y)

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
inst✝ : Nontrivial E
x : M
p : ∃ᶠ (x_1 : E) in 𝓝 (↑(extChartAt I x) x), x_1 ≠ ↑(extChartAt I x) x
y : E
m : y ∈ (extChartAt I x).target
h : ↑(extChartAt I x).symm y = x
⊢ y = ↑(extChartAt I x) (↑(extChartAt I x).symm y)
Tactic:
rw [PartialEquiv.right_inv _ m]
State after:
no goals