Theorem: IsPreconnected.directed_iInter (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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
p : ∀ (a : I), IsPreconnected (s a)
c : ∀ (a : I), IsCompact (s a)
⊢ IsPreconnected (⋂ a, s a)
Tactic:
contrapose p
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Tactic:
have ci : IsClosed (⋂ a, s a) := isClosed_iInter fun i ↦ (c i).isClosed
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
ci : IsClosed (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
ci : IsClosed (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Tactic:
simp only [isPreconnected_iff_subset_of_fully_disjoint_open ci, not_forall] at p
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ¬∀ (a : I), IsPreconnected (s a)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Tactic:
simp only [isPreconnected_iff_subset_of_fully_disjoint_open (c _).isClosed, not_forall]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
rcases p with ⟨u, v, uo, vo, suv, uv, no⟩
State after:
case 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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)

State before:
case 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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
have e : ∃ a, s a ⊆ u ∪ v := by
  by_contra h; simp only [not_exists, Set.not_subset] at h
  suffices n : (⋂ a, s a \ (u ∪ v)).Nonempty by
    rcases n with ⟨x, n⟩; simp only [mem_iInter, mem_diff, forall_and, forall_const] at n
    rw [← mem_iInter] at n; simp only [suv n.1, not_true, imp_false] at n; exact n.2
  apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
  intro a b; rcases d a b with ⟨c, ac, bc⟩
  use c, diff_subset_diff_left ac, diff_subset_diff_left bc
  intro a; rcases h a with ⟨x, xa, xuv⟩; exact ⟨x, mem_diff_of_mem xa xuv⟩
  intro a; exact (c a).diff (uo.union vo)
  intro a; exact ((c a).diff (uo.union vo)).isClosed
State after:
case 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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
e : ∃ a, s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)

State before:
case 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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
e : ∃ a, s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
rcases e with ⟨a, auv⟩
State after:
case intro.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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)

State before:
case intro.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✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
use a, u, v, uo, vo, auv, uv
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ¬(s a ⊆ u ∨ s a ⊆ v)

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ¬(s a ⊆ u ∨ s a ⊆ v)
Tactic:
contrapose no
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
no : ¬¬(s a ⊆ u ∨ s a ⊆ v)
⊢ ¬¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
no : ¬¬(s a ⊆ u ∨ s a ⊆ v)
⊢ ¬¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
Tactic:
simp only [not_not] at no ⊢
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
no : s a ⊆ u ∨ s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
no : s a ⊆ u ∨ s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
cases' no with su sv
State after:
case h.inl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

case h.inr
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

State before:
case h.inl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

case h.inr
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
left
State after:
case h.inl.h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u

case h.inr
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

State before:
case h.inl.h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u

case h.inr
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
exact _root_.trans (iInter_subset _ _) su
State after:
case h.inr
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

State before:
case h.inr
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
right
State after:
case h.inr.h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ v

State before:
case h.inr.h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ v
Tactic:
exact _root_.trans (iInter_subset _ _) sv
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
⊢ ∃ a, s a ⊆ u ∪ v
Tactic:
by_contra h
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ¬∃ a, s a ⊆ u ∪ v
⊢ False

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ¬∃ a, s a ⊆ u ∪ v
⊢ False
Tactic:
simp only [not_exists, Set.not_subset] at h
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ False

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ False
Tactic:
suffices n : (⋂ a, s a \ (u ∪ v)).Nonempty by
  rcases n with ⟨x, n⟩; simp only [mem_iInter, mem_diff, forall_and, forall_const] at n
  rw [← mem_iInter] at n; simp only [suv n.1, not_true, imp_false] at n; exact n.2
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ (⋂ a, s a \ (u ∪ v)).Nonempty

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ (⋂ a, s a \ (u ∪ v)).Nonempty
Tactic:
apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
State after:
case htd
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => s i \ (u ∪ v)

case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htd
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => s i \ (u ∪ v)

case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
intro a b
State after:
case htd
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a b : I
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) a) ((fun i => s i \ (u ∪ v)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) b) ((fun i => s i \ (u ∪ v)) z)

case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htd
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a b : I
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) a) ((fun i => s i \ (u ∪ v)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) b) ((fun i => s i \ (u ∪ v)) z)

case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
rcases d a b with ⟨c, ac, bc⟩
State after:
case htd.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c✝ : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a b c : I
ac : s a ⊇ s c
bc : s b ⊇ s c
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) a) ((fun i => s i \ (u ∪ v)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) b) ((fun i => s i \ (u ∪ v)) z)

case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htd.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c✝ : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a b c : I
ac : s a ⊇ s c
bc : s b ⊇ s c
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) a) ((fun i => s i \ (u ∪ v)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) b) ((fun i => s i \ (u ∪ v)) z)

case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
use c, diff_subset_diff_left ac, diff_subset_diff_left bc
State after:
case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
intro a
State after:
case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ (s a \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htn
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ (s a \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
rcases h a with ⟨x, xa, xuv⟩
State after:
case htn.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
x : X
xa : x ∈ s a
xuv : x ∉ u ∪ v
⊢ (s a \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htn.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
x : X
xa : x ∈ s a
xuv : x ∉ u ∪ v
⊢ (s a \ (u ∪ v)).Nonempty

case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
exact ⟨x, mem_diff_of_mem xa xuv⟩
State after:
case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
intro a
State after:
case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ IsCompact (s a \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htc
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ IsCompact (s a \ (u ∪ v))

case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
exact (c a).diff (uo.union vo)
State after:
case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))

State before:
case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
intro a
State after:
case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ IsClosed (s a \ (u ∪ v))

State before:
case htcl
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ IsClosed (s a \ (u ∪ v))
Tactic:
exact ((c a).diff (uo.union vo)).isClosed
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
n : (⋂ a, s a \ (u ∪ v)).Nonempty
⊢ False
Tactic:
rcases n with ⟨x, n⟩
State after:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : x ∈ ⋂ a, s a \ (u ∪ v)
⊢ False

State before:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : x ∈ ⋂ a, s a \ (u ∪ v)
⊢ False
Tactic:
simp only [mem_iInter, mem_diff, forall_and, forall_const] at n
State after:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : (∀ (x_1 : I), x ∈ s x_1) ∧ x ∉ u ∪ v
⊢ False

State before:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : (∀ (x_1 : I), x ∈ s x_1) ∧ x ∉ u ∪ v
⊢ False
Tactic:
rw [← mem_iInter] at n
State after:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : x ∈ ⋂ i, s i ∧ x ∉ u ∪ v
⊢ False

State before:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : x ∈ ⋂ i, s i ∧ x ∉ u ∪ v
⊢ False
Tactic:
simp only [suv n.1, not_true, imp_false] at n
State after:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : x ∈ ⋂ i, s i ∧ False
⊢ False

State before:
case intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
x : X
n : x ∈ ⋂ i, s i ∧ False
⊢ False
Tactic:
exact n.2
State after:
no goals