Theorem: Nonseparating.complexManifold
Proof 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
Proof 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