Theorem: IsPreconnected.open_diff_line (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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ IsPreconnected (s \ {p | p.2 = a})
Tactic:
apply IsPreconnected.open_diff sc so
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ Nonseparating {p | p.2 = a}

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ Nonseparating {p | p.2 = a}
Tactic:
have e : {p : ℂ × S | p.2 = a} = univ ×ˢ {a} := by
  apply Set.ext; intro ⟨c, z⟩
  simp only [mem_prod_eq, mem_setOf, mem_univ, true_and_iff, mem_singleton_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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating {p | p.2 = a}

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating {p | p.2 = a}
Tactic:
rw [e]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating (univ ×ˢ {a})

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating (univ ×ˢ {a})
Tactic:
exact Nonseparating.univ_prod (AnalyticManifold.nonseparating_singleton _)
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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ {p | p.2 = a} = univ ×ˢ {a}
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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ ∀ (x : ℂ × S), x ∈ {p | p.2 = a} ↔ x ∈ univ ×ˢ {a}

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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ ∀ (x : ℂ × S), x ∈ {p | p.2 = a} ↔ x ∈ univ ×ˢ {a}
Tactic:
intro ⟨c, 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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
c : ℂ
z : S
⊢ (c, z) ∈ {p | p.2 = a} ↔ (c, z) ∈ univ ×ˢ {a}

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
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
c : ℂ
z : S
⊢ (c, z) ∈ {p | p.2 = a} ↔ (c, z) ∈ univ ×ˢ {a}
Tactic:
simp only [mem_prod_eq, mem_setOf, mem_univ, true_and_iff, mem_singleton_iff]
State after:
no goals