case basic
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ : Set α
a✝ : s✝ ∈ ↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)
⊢ s✝ = ∅ ∨ s✝ = univ

case univ
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ

case inter
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
a_ih✝¹ : s✝ = ∅ ∨ s✝ = univ
a_ih✝ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
h : IsOpen U
⊢ U = ∅ ∨ U = univ
induction h
case univ
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ

case inter
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
a_ih✝¹ : s✝ = ∅ ∨ s✝ = univ
a_ih✝ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case basic
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ : Set α
a✝ : s✝ ∈ ↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)
⊢ s✝ = ∅ ∨ s✝ = univ

case univ
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ

case inter
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
a_ih✝¹ : s✝ = ∅ ∨ s✝ = univ
a_ih✝ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case basic h => exact False.elim h
case inter
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
a_ih✝¹ : s✝ = ∅ ∨ s✝ = univ
a_ih✝ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case univ
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ

case inter
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
a_ih✝¹ : s✝ = ∅ ∨ s✝ = univ
a_ih✝ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case univ => exact .inr rfl
case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case inter
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
a_ih✝¹ : s✝ = ∅ ∨ s✝ = univ
a_ih✝ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case inter h₁ h₂ =>
  rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
no goals
case sUnion
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
case sUnion _ ih => exact sUnion_mem_empty_univ ih
no goals
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ : Set α
h : s✝ ∈ ↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)
⊢ s✝ = ∅ ∨ s✝ = univ
exact False.elim h
no goals
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ univ = ∅ ∨ univ = univ
exact .inr rfl
no goals
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) t✝
h₁ : s✝ = ∅ ∨ s✝ = univ
h₂ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ
rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
no goals
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen (↑OrderDual.ofDual (↑OrderDual.ofDual ⊥)) s
ih : ∀ (s : Set α), s ∈ S✝ → s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ
exact sUnion_mem_empty_univ ih
case inl
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
⊢ IsOpen ∅

case inr
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
⊢ IsOpen univ
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
U : Set α
⊢ U = ∅ ∨ U = univ → IsOpen U
rintro (rfl | rfl)
no goals
case inl
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
⊢ IsOpen ∅

case inr
α✝ : Type ?u.11392
t t₁ t₂ : TopologicalSpace α✝
s : Set α✝
α : Type u_1
⊢ IsOpen univ
exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]