Theorem: Nonseparating.univ_prod (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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ Nonseparating (univ ×ˢ t)
Tactic:
have e : ((univ : Set X) ×ˢ t)ᶜ = univ ×ˢ tᶜ := by
  apply Set.ext; intro ⟨a, x⟩; rw [mem_compl_iff]
  simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and_iff]
State after:
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ᶜ
⊢ Nonseparating (univ ×ˢ t)

State before:
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ᶜ
⊢ Nonseparating (univ ×ˢ t)
Tactic:
constructor
State after:
case dense
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ᶜ
⊢ Dense (univ ×ˢ t)ᶜ

case loc
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ᶜ
⊢ ∀ (x : X × Y) (u : Set (X × Y)),
    x ∈ univ ×ˢ t → u ∈ 𝓝 x → ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] x ∧ 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ ∀ (x : X × Y), x ∈ (univ ×ˢ t)ᶜ ↔ x ∈ univ ×ˢ 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ ∀ (x : X × Y), x ∈ (univ ×ˢ t)ᶜ ↔ x ∈ univ ×ˢ tᶜ
Tactic:
intro ⟨a, 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∈ (univ ×ˢ t)ᶜ ↔ (a, x) ∈ univ ×ˢ 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∈ (univ ×ˢ t)ᶜ ↔ (a, x) ∈ univ ×ˢ tᶜ
Tactic:
rw [mem_compl_iff]
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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∉ univ ×ˢ t ↔ (a, x) ∈ univ ×ˢ 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
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∉ univ ×ˢ t ↔ (a, x) ∈ univ ×ˢ tᶜ
Tactic:
simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and_iff]
State after:
no goals

State before:
case dense
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ᶜ
⊢ Dense (univ ×ˢ t)ᶜ
Tactic:
rw [e]
State after:
case dense
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ᶜ
⊢ Dense (univ ×ˢ tᶜ)

State before:
case dense
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ᶜ
⊢ Dense (univ ×ˢ tᶜ)
Tactic:
exact dense_univ.prod n.dense
State after:
no goals

State before:
case loc
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ᶜ
⊢ ∀ (x : X × Y) (u : Set (X × Y)),
    x ∈ univ ×ˢ t → u ∈ 𝓝 x → ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] x ∧ IsPreconnected c
Tactic:
intro ⟨a, x⟩ u m un
State after:
case loc
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)
m : (a, x) ∈ univ ×ˢ t
un : u ∈ 𝓝 (a, x)
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c

State before:
case loc
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)
m : (a, x) ∈ univ ×ˢ t
un : u ∈ 𝓝 (a, x)
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
simp only [mem_prod_eq, mem_univ, true_and_iff] at m
State after:
case loc
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c

State before:
case loc
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
rcases mem_nhds_prod_iff.mp un with ⟨u0, n0, u1, n1, uu⟩
State after:
case loc.intro.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
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c

State before:
case loc.intro.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
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
rcases n.loc x u1 m n1 with ⟨c1, cs1, cn1, cp1⟩
State after:
case loc.intro.intro.intro.intro.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
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c

State before:
case loc.intro.intro.intro.intro.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
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
rcases locallyConnectedSpace_iff_open_connected_subsets.mp (by infer_instance) a u0 n0 with
  ⟨c0, cs0, co0, cm0, cc0⟩
State after:
case loc.intro.intro.intro.intro.intro.intro.intro.intro.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
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c

State before:
case loc.intro.intro.intro.intro.intro.intro.intro.intro.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
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
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
use c0 ×ˢ c1
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
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 ⊆ u \ univ ×ˢ t ∧ c0 ×ˢ c1 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected (c0 ×ˢ c1)

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
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 ⊆ u \ univ ×ˢ t ∧ c0 ×ˢ c1 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected (c0 ×ˢ c1)
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
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 ⊆ u \ univ ×ˢ 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
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 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x)

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)

State before:
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
⊢ LocallyConnectedSpace X
Tactic:
infer_instance
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
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 ⊆ u \ univ ×ˢ t
Tactic:
intro ⟨b, y⟩ m'
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
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
b : X
y : Y
m' : (b, y) ∈ c0 ×ˢ c1
⊢ (b, y) ∈ u \ univ ×ˢ 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
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
b : X
y : Y
m' : (b, y) ∈ c0 ×ˢ c1
⊢ (b, y) ∈ u \ univ ×ˢ t
Tactic:
simp only [mem_prod_eq, mem_diff, mem_univ, true_and_iff] at m' ⊢
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
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
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u ∧ y ∉ 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
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
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u ∧ y ∉ t
Tactic:
refine ⟨?_, (cs1 m'.2).2⟩
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
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
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u

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
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
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u
Tactic:
apply uu
State after:
case h.refine_1.a
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
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u0 ×ˢ u1

State before:
case h.refine_1.a
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
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u0 ×ˢ u1
Tactic:
use cs0 m'.1, (cs1 m'.2).1
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
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 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x)
Tactic:
rw [e, nhdsWithin_prod_eq, nhdsWithin_univ]
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
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

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
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
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
State after:
no goals