internlm/Lean-Github huggingface dataset:
Theorem: Nonseparating.univ_prod
Proof 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ∈ 𝓝 a ×ˢ 𝓝[tᶜ] x
Tactic:
exact Filter.prod_mem_prod (co0.mem_nhds cm0) cn1
Proof state after:
no goals
Theorem: Nonseparating.univ_prod
Proof 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ IsPreconnected (c0 ×ˢ c1)
Tactic:
exact cc0.isPreconnected.prod cp1
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
Proof 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]
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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⟩
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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]
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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⟩
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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ᶜ
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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ᶜ
Theorem: Nonseparating.complexManifold
Proof 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⟩
Proof 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ᶜ
Theorem: Nonseparating.complexManifold
Proof 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]
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
Proof 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]
Proof 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)
Theorem: Nonseparating.complexManifold
Proof 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
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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]
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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]
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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
Proof 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
Theorem: Nonseparating.complexManifold
Proof 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⟩
Proof 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