Theorem: isPreconnected_iff_subset_of_fully_disjoint_open (Ray/Misc/Connected.lean)

State before:
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ IsPreconnected s ↔ ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed sc]
State after:
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

State before:
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
constructor
State after:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

case mpr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ (∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

State before:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
intro h u v uo vo suv uv
State after:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have suc : IsClosed (s ∩ u) := isClosed_closed_inter sc vo uv suv
State after:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have svc : IsClosed (s ∩ v) := isClosed_closed_inter sc uo uv.symm ((union_comm u v).subst suv)
State after:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have h0 : s ⊆ s ∩ u ∪ s ∩ v := by
  simp only [←inter_union_distrib_left]; exact subset_inter (subset_refl _) suv
State after:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have h1 : Disjoint (s ∩ u) (s ∩ v) := Disjoint.inter_left' _ (Disjoint.inter_right' _ uv)
State after:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mp
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
cases' h (s ∩ u) (s ∩ v) suc svc h0 h1 with su sv
State after:
case mp.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u ∨ s ⊆ v

case mp.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v

State before:
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ s ∩ u ∪ s ∩ v
Tactic:
simp only [←inter_union_distrib_left]
State after:
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ s ∩ (u ∪ v)

State before:
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ s ∩ (u ∪ v)
Tactic:
exact subset_inter (subset_refl _) suv
State after:
no goals

State before:
case mp.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
left
State after:
case mp.inl.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u

State before:
case mp.inl.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u
Tactic:
exact (subset_inter_iff.mp su).2
State after:
no goals

State before:
case mp.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
right
State after:
case mp.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ v

State before:
case mp.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ v
Tactic:
exact (subset_inter_iff.mp sv).2
State after:
no goals

State before:
case mpr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
⊢ (∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
intro h u v uc vc suv uv
State after:
case mpr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mpr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
rcases NormalSpace.normal u v uc vc uv with ⟨u', v', uo, vo, uu, vv, uv'⟩
State after:
case mpr.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mpr.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
cases' h u' v' uo vo (_root_.trans suv (union_subset_union uu vv)) uv' with h h
State after:
case mpr.intro.intro.intro.intro.intro.intro.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
⊢ s ⊆ u ∨ s ⊆ v

case mpr.intro.intro.intro.intro.intro.intro.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ u ∨ s ⊆ v

State before:
case mpr.intro.intro.intro.intro.intro.intro.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
left
State after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
⊢ s ⊆ u

State before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
⊢ s ⊆ u
Tactic:
intro x m
State after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
⊢ x ∈ u

State before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
⊢ x ∈ u
Tactic:
cases' (mem_union _ _ _).mp (suv m) with mu mv
State after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ u

case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u

State before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ u

case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u
Tactic:
exact mu
State after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u

State before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u
Tactic:
exfalso
State after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ False

State before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ False
Tactic:
exact disjoint_left.mp uv' (h m) (vv mv)
State after:
no goals

State before:
case mpr.intro.intro.intro.intro.intro.intro.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
right
State after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ v

State before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ v
Tactic:
intro x m
State after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
⊢ x ∈ v

State before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
⊢ x ∈ v
Tactic:
cases' (mem_union _ _ _).mp (suv m) with mu mv
State after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ v

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v

State before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ v

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Tactic:
exfalso
State after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ False

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v

State before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ False

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Tactic:
exact disjoint_right.mp uv' (h m) (uu mu)
State after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v

State before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Tactic:
exact mv
State after:
no goals