-- Mathlib/Topology/Order/ScottTopology.lean
lemma isOpen_iff_Iic_compl_or_univ [TopologicalSpace α] [Topology.IsScott α univ] (U : Set α) :
    IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Proof state:
case mpr.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen univ

Tactic:
exact isOpen_univ

Result:
no goals

Proof state:
case mp.inr.h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ ∃ a, (Iic a)ᶜ = U

Tactic:
use sSup Uᶜ

Result:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ (Iic (sSup Uᶜ))ᶜ = U

Proof state:
case mpr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ (U = univ ∨ ∃ a, (Iic a)ᶜ = U) → IsOpen U

Tactic:
rintro (rfl | ⟨a, rfl⟩)

Result:
case mpr.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen univ

case mpr.inr.intro
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
a : α
⊢ IsOpen (Iic a)ᶜ

Proof state:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ (Iic (sSup Uᶜ))ᶜ = U

Tactic:
rw [compl_eq_comm, le_antisymm_iff]

Result:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ Uᶜ ≤ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ≤ Uᶜ

Proof state:
case mp
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ IsOpen U → U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
intro hU

Result:
case mp
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Proof state:
case mpr.inr.intro
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
a : α
⊢ IsOpen (Iic a)ᶜ

Tactic:
exact isClosed_Iic.isOpen_compl

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ Uᶜ ≤ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ≤ Uᶜ

Tactic:
exact ⟨fun _ ha ↦ le_sSup ha, (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset
  (dirSupClosed_iff_forall_sSup.mp (dirSupClosed_of_isClosed hU.isClosed_compl)
  neUc (isChain_of_trichotomous Uᶜ).directedOn le_rfl)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ IsOpen U → U = univ ∨ ∃ a, (Iic a)ᶜ = U

case mpr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ (U = univ ∨ ∃ a, (Iic a)ᶜ = U) → IsOpen U

Proof state:
case mp.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
eUc : Uᶜ = ∅
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
exact Or.inl (compl_empty_iff.mp eUc)

Result:
no goals

Proof state:
case mp.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
apply Or.inr

Result:
case mp.inr.h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ ∃ a, (Iic a)ᶜ = U

Proof state:
case mp
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
rcases eq_empty_or_nonempty Uᶜ with eUc | neUc

Result:
case mp.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
eUc : Uᶜ = ∅
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

case mp.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen U
neUc : Uᶜ.Nonempty
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U