Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr.inr.hs.ho
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t

pp: case inr.inr.hs.hc
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsCompact t

pp: case inr.inr.hs.h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsOpen[inst✝¹] t

Tactic:
<;>

Goal state after:
case inr.inr.hs.ho
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t

case inr.inr.hs.hc
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsCompact t

case inr.inr.hs.h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsOpen[inst✝¹] t