Theorem: Nonseparating.complexManifold (Ray/AnalyticManifold/Nonseparating.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ Dense tᶜ
Tactic:
rw [dense_iff_inter_open]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ ∀ (U : Set S), IsOpen U → U.Nonempty → (U ∩ tᶜ).Nonempty

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ ∀ (U : Set S), IsOpen U → U.Nonempty → (U ∩ tᶜ).Nonempty
Tactic:
intro u uo ⟨z, m⟩
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
⊢ (u ∩ tᶜ).Nonempty

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
⊢ (u ∩ tᶜ).Nonempty
Tactic:
by_cases zt : z ∉ t
State after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∉ t
⊢ (u ∩ tᶜ).Nonempty

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : ¬z ∉ t
⊢ (u ∩ tᶜ).Nonempty

State before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∉ t
⊢ (u ∩ tᶜ).Nonempty

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : ¬z ∉ t
⊢ (u ∩ tᶜ).Nonempty
Tactic:
use z, m, zt
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : ¬z ∉ t
⊢ (u ∩ tᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : ¬z ∉ t
⊢ (u ∩ tᶜ).Nonempty
Tactic:
simp only [not_not] at zt
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
⊢ (u ∩ tᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
⊢ (u ∩ tᶜ).Nonempty
Tactic:
generalize hv : (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' u = v
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
⊢ (u ∩ tᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
⊢ (u ∩ tᶜ).Nonempty
Tactic:
have vo : IsOpen v := by
  rw [← hv]
  exact (continuousOn_extChartAt_symm I z).isOpen_inter_preimage
    (isOpen_extChartAt_target I z) uo
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
⊢ (u ∩ tᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
⊢ (u ∩ tᶜ).Nonempty
Tactic:
have vn : v.Nonempty := by
  use extChartAt I z z
  simp only [mem_inter_iff, mem_extChartAt_target, true_and_iff, mem_preimage,
    PartialEquiv.left_inv _ (mem_extChartAt_source I z), m, ← hv]
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
⊢ (u ∩ tᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
⊢ (u ∩ tᶜ).Nonempty
Tactic:
rcases dense_iff_inter_open.mp (h z).dense v vo vn with ⟨y, m⟩
State after:
case neg.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m✝ : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
m : y ∈ v ∩ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ
⊢ (u ∩ tᶜ).Nonempty

State before:
case neg.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m✝ : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
m : y ∈ v ∩ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ
⊢ (u ∩ tᶜ).Nonempty
Tactic:
use(extChartAt I z).symm y
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m✝ : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
m : y ∈ v ∩ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ
⊢ ↑(extChartAt I z).symm y ∈ u ∩ tᶜ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m✝ : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
m : y ∈ v ∩ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ
⊢ ↑(extChartAt I z).symm y ∈ u ∩ tᶜ
Tactic:
simp only [mem_inter_iff, mem_preimage, mem_compl_iff, not_and, ← hv] at m
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m✝ : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
m :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    (y ∈ (extChartAt I z).target → ↑(extChartAt I z).symm y ∉ t)
⊢ ↑(extChartAt I z).symm y ∈ u ∩ tᶜ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m✝ : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
m :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    (y ∈ (extChartAt I z).target → ↑(extChartAt I z).symm y ∉ t)
⊢ ↑(extChartAt I z).symm y ∈ u ∩ tᶜ
Tactic:
rcases m with ⟨⟨ym, yu⟩, yt⟩
State after:
case h.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
yt : y ∈ (extChartAt I z).target → ↑(extChartAt I z).symm y ∉ t
ym : y ∈ (extChartAt I z).target
yu : ↑(extChartAt I z).symm y ∈ u
⊢ ↑(extChartAt I z).symm y ∈ u ∩ tᶜ

State before:
case h.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
yt : y ∈ (extChartAt I z).target → ↑(extChartAt I z).symm y ∉ t
ym : y ∈ (extChartAt I z).target
yu : ↑(extChartAt I z).symm y ∈ u
⊢ ↑(extChartAt I z).symm y ∈ u ∩ tᶜ
Tactic:
simp only [mem_inter_iff, ym, yu, true_and_iff, mem_compl_iff]
State after:
case h.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
yt : y ∈ (extChartAt I z).target → ↑(extChartAt I z).symm y ∉ t
ym : y ∈ (extChartAt I z).target
yu : ↑(extChartAt I z).symm y ∈ u
⊢ ↑(extChartAt I z).symm y ∉ t

State before:
case h.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
vn : v.Nonempty
y : ℂ
yt : y ∈ (extChartAt I z).target → ↑(extChartAt I z).symm y ∉ t
ym : y ∈ (extChartAt I z).target
yu : ↑(extChartAt I z).symm y ∈ u
⊢ ↑(extChartAt I z).symm y ∉ t
Tactic:
exact yt ym
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
⊢ IsOpen v
Tactic:
rw [← hv]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
⊢ IsOpen ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
⊢ IsOpen ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u)
Tactic:
exact (continuousOn_extChartAt_symm I z).isOpen_inter_preimage
  (isOpen_extChartAt_target I z) uo
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
⊢ v.Nonempty
Tactic:
use extChartAt I z z
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
⊢ ↑(extChartAt I z) z ∈ v

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
u : Set S
uo : IsOpen u
z : S
m : z ∈ u
zt : z ∈ t
v : Set ℂ
hv : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u = v
vo : IsOpen v
⊢ ↑(extChartAt I z) z ∈ v
Tactic:
simp only [mem_inter_iff, mem_extChartAt_target, true_and_iff, mem_preimage,
  PartialEquiv.left_inv _ (mem_extChartAt_source I z), m, ← hv]
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ ∀ (x : S) (u : Set S), x ∈ t → u ∈ 𝓝 x → ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] x ∧ IsPreconnected c
Tactic:
intro z u zt un
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c
Tactic:
have m : extChartAt I z z ∈ (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' t := by
  simp only [mem_inter_iff, mem_extChartAt_target I z, true_and_iff, mem_preimage,
    PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c
Tactic:
have n : (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' u ∈ 𝓝 (extChartAt I z z) := by
  apply Filter.inter_mem
  exact (isOpen_extChartAt_target I z).mem_nhds (mem_extChartAt_target I z)
  exact extChartAt_preimage_mem_nhds _ un
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c
Tactic:
rcases (h z).loc _ _ m n with ⟨c, cs, cn, cp⟩
State after:
case intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c

State before:
case intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c
Tactic:
use(extChartAt I z).source ∩ extChartAt I z ⁻¹' c
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ⊆ u \ t ∧
    (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ∈ 𝓝[tᶜ] z ∧
      IsPreconnected ((extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c)

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ⊆ u \ t ∧
    (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ∈ 𝓝[tᶜ] z ∧
      IsPreconnected ((extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c)
Tactic:
refine ⟨?_, ?_, ?_⟩
State after:
case h.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ⊆ u \ t

case h.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ∈ 𝓝[tᶜ] z

case h.refine_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ IsPreconnected ((extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
⊢ ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
Tactic:
simp only [mem_inter_iff, mem_extChartAt_target I z, true_and_iff, mem_preimage,
  PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt]
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Tactic:
apply Filter.inter_mem
State after:
case hs
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ (extChartAt I z).target ∈ 𝓝 (↑(extChartAt I z) z)

case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)

State before:
case hs
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ (extChartAt I z).target ∈ 𝓝 (↑(extChartAt I z) z)

case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Tactic:
exact (isOpen_extChartAt_target I z).mem_nhds (mem_extChartAt_target I z)
State after:
case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)

State before:
case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Tactic:
exact extChartAt_preimage_mem_nhds _ un
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ ∀ (x : S), x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ ∀ (x : S), x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c
Tactic:
intro x
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c
Tactic:
simp only [mem_inter_iff, mem_preimage, mem_image]
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c ↔ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c ↔ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Tactic:
constructor
State after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c → ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ (∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x) → x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c

State before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c → ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Tactic:
intro ⟨xz, xc⟩
State after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x

State before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Tactic:
refine ⟨_, xc, ?_⟩
State after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) x) = x

State before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) x) = x
Tactic:
simp only [PartialEquiv.left_inv _ xz]
State after:
no goals

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ (∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x) → x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
Tactic:
intro ⟨y, yc, yx⟩
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
Tactic:
rw [← yx]
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Tactic:
have xc := cs yc
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  y ∈
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  y ∈
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Tactic:
simp only [mem_diff, mem_inter_iff, mem_preimage] at xc
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    ¬(y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ t)
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    ¬(y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ t)
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Tactic:
have yz := xc.1.1
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    ¬(y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ t)
yz : y ∈ (extChartAt I z).target
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    ¬(y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ t)
yz : y ∈ (extChartAt I z).target
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Tactic:
use PartialEquiv.map_target _ yz
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    ¬(y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ t)
yz : y ∈ (extChartAt I z).target
⊢ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  (y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ u) ∧
    ¬(y ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm y ∈ t)
yz : y ∈ (extChartAt I z).target
⊢ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Tactic:
simp only [PartialEquiv.right_inv _ yz, yc]
State after:
no goals

State before:
case h.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ⊆ u \ t
Tactic:
intro x xm
State after:
case h.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xm : x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c
⊢ x ∈ u \ t

State before:
case h.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xm : x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c
⊢ x ∈ u \ t
Tactic:
simp only [mem_inter_iff, mem_preimage] at xm
State after:
case h.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xm : x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
⊢ x ∈ u \ t

State before:
case h.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xm : x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
⊢ x ∈ u \ t
Tactic:
rcases xm with ⟨xz, xc⟩
State after:
case h.refine_1.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ x ∈ u \ t

State before:
case h.refine_1.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ x ∈ u \ t
Tactic:
replace xc := cs xc
State after:
case h.refine_1.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xz : x ∈ (extChartAt I z).source
xc :
  ↑(extChartAt I z) x ∈
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ x ∈ u \ t

State before:
case h.refine_1.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xz : x ∈ (extChartAt I z).source
xc :
  ↑(extChartAt I z) x ∈
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ x ∈ u \ t
Tactic:
simp only [mem_diff, mem_inter_iff, mem_preimage, PartialEquiv.map_source _ xz, true_and_iff,
  PartialEquiv.left_inv _ xz] at xc
State after:
case h.refine_1.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xz : x ∈ (extChartAt I z).source
xc : x ∈ u ∧ x ∉ t
⊢ x ∈ u \ t

State before:
case h.refine_1.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
x : S
xz : x ∈ (extChartAt I z).source
xc : x ∈ u ∧ x ∉ t
⊢ x ∈ u \ t
Tactic:
exact xc
State after:
no goals

State before:
case h.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ∈ 𝓝[tᶜ] z
Tactic:
rw [e]
State after:
case h.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ ↑(extChartAt I z).symm '' c ∈ 𝓝[tᶜ] z

State before:
case h.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ ↑(extChartAt I z).symm '' c ∈ 𝓝[tᶜ] z
Tactic:
convert Filter.image_mem_map cn
State after:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ 𝓝[tᶜ] z =
    Filter.map (↑(extChartAt I z).symm)
      (𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z)

State before:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ 𝓝[tᶜ] z =
    Filter.map (↑(extChartAt I z).symm)
      (𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z)
Tactic:
have ee : ⇑(extChartAt I z).symm = (extChartAt' I z).symm := rfl
State after:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ 𝓝[tᶜ] z =
    Filter.map (↑(extChartAt I z).symm)
      (𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z)

State before:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ 𝓝[tᶜ] z =
    Filter.map (↑(extChartAt I z).symm)
      (𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z)
Tactic:
rw [ee, (extChartAt' I z).symm.map_nhdsWithin_eq (mem_extChartAt_target I z), ← ee]
State after:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ 𝓝[tᶜ] z =
    𝓝[↑(extChartAt I z).symm ''
        ((extChartAt' I z).symm.source ∩ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ)]
      ↑(extChartAt I z).symm (↑(extChartAt I z) z)

State before:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ 𝓝[tᶜ] z =
    𝓝[↑(extChartAt I z).symm ''
        ((extChartAt' I z).symm.source ∩ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ)]
      ↑(extChartAt I z).symm (↑(extChartAt I z) z)
Tactic:
simp only [extChartAt', PartialHomeomorph.symm_source,
  PartialEquiv.left_inv _ (mem_extChartAt_source I z), compl_inter, inter_union_distrib_left,
  inter_compl_self, empty_union, image_inter]
State after:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ 𝓝[tᶜ] z = 𝓝[↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ)] z

State before:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ 𝓝[tᶜ] z = 𝓝[↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ)] z
Tactic:
apply nhdsWithin_eq_nhdsWithin (mem_extChartAt_source I z) (isOpen_extChartAt_source I z)
State after:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ tᶜ ∩ (extChartAt I z).source =
    ↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ) ∩ (extChartAt I z).source

State before:
case h.e'_5
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ tᶜ ∩ (extChartAt I z).source =
    ↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ) ∩ (extChartAt I z).source
Tactic:
apply Set.ext
State after:
case h.e'_5.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ ∀ (x : S),
    x ∈ tᶜ ∩ (extChartAt I z).source ↔
      x ∈
        ↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ) ∩ (extChartAt I z).source

State before:
case h.e'_5.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
⊢ ∀ (x : S),
    x ∈ tᶜ ∩ (extChartAt I z).source ↔
      x ∈
        ↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ) ∩ (extChartAt I z).source
Tactic:
intro x
State after:
case h.e'_5.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ x ∈ tᶜ ∩ (extChartAt I z).source ↔
    x ∈ ↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ) ∩ (extChartAt I z).source

State before:
case h.e'_5.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ x ∈ tᶜ ∩ (extChartAt I z).source ↔
    x ∈ ↑(extChartAt I z).symm '' ((extChartAt I z).target ∩ (↑(extChartAt I z).symm ⁻¹' t)ᶜ) ∩ (extChartAt I z).source
Tactic:
simp only [mem_inter_iff, mem_compl_iff, mem_image, mem_preimage]
State after:
case h.e'_5.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source ↔
    (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
      x ∈ (extChartAt I z).source

State before:
case h.e'_5.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source ↔
    (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
      x ∈ (extChartAt I z).source
Tactic:
constructor
State after:
case h.e'_5.h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source →
    (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
      x ∈ (extChartAt I z).source

case h.e'_5.h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
      x ∈ (extChartAt I z).source →
    x ∉ t ∧ x ∈ (extChartAt I z).source

State before:
case h.e'_5.h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source →
    (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
      x ∈ (extChartAt I z).source
Tactic:
intro ⟨xt, xz⟩
State after:
case h.e'_5.h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
xt : x ∉ t
xz : x ∈ (extChartAt I z).source
⊢ (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
    x ∈ (extChartAt I z).source

State before:
case h.e'_5.h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
xt : x ∉ t
xz : x ∈ (extChartAt I z).source
⊢ (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
    x ∈ (extChartAt I z).source
Tactic:
refine ⟨⟨extChartAt I z x, ?_⟩, xz⟩
State after:
case h.e'_5.h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
xt : x ∉ t
xz : x ∈ (extChartAt I z).source
⊢ (↑(extChartAt I z) x ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm (↑(extChartAt I z) x) ∉ t) ∧
    ↑(extChartAt I z).symm (↑(extChartAt I z) x) = x

State before:
case h.e'_5.h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
xt : x ∉ t
xz : x ∈ (extChartAt I z).source
⊢ (↑(extChartAt I z) x ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm (↑(extChartAt I z) x) ∉ t) ∧
    ↑(extChartAt I z).symm (↑(extChartAt I z) x) = x
Tactic:
simp only [PartialEquiv.left_inv _ xz, xt, PartialEquiv.map_source _ xz, not_false_iff,
  and_self_iff, eq_self_iff_true]
State after:
no goals

State before:
case h.e'_5.h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
⊢ (∃ x_1, (x_1 ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x_1 ∉ t) ∧ ↑(extChartAt I z).symm x_1 = x) ∧
      x ∈ (extChartAt I z).source →
    x ∉ t ∧ x ∈ (extChartAt I z).source
Tactic:
intro ⟨⟨y, ⟨⟨yz, yt⟩, yx⟩⟩, _⟩
State after:
case h.e'_5.h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
y : ℂ
yz : y ∈ (extChartAt I z).target
yt : ↑(extChartAt I z).symm y ∉ t
yx : ↑(extChartAt I z).symm y = x
right✝ : x ∈ (extChartAt I z).source
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source

State before:
case h.e'_5.h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
y : ℂ
yz : y ∈ (extChartAt I z).target
yt : ↑(extChartAt I z).symm y ∉ t
yx : ↑(extChartAt I z).symm y = x
right✝ : x ∈ (extChartAt I z).source
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source
Tactic:
simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and_iff]
State after:
no goals

State before:
case h.refine_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ IsPreconnected ((extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c)
Tactic:
rw [e]
State after:
case h.refine_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ IsPreconnected (↑(extChartAt I z).symm '' c)

State before:
case h.refine_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ IsPreconnected (↑(extChartAt I z).symm '' c)
Tactic:
apply cp.image
State after:
case h.refine_3.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ ContinuousOn (↑(extChartAt I z).symm) c

State before:
case h.refine_3.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ ContinuousOn (↑(extChartAt I z).symm) c
Tactic:
apply (continuousOn_extChartAt_symm I z).mono
State after:
case h.refine_3.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ c ⊆ (extChartAt I z).target

State before:
case h.refine_3.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ c ⊆ (extChartAt I z).target
Tactic:
exact _root_.trans cs (_root_.trans (diff_subset _ _) (inter_subset_left _ _))
State after:
no goals