ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
t : TopologicalSpace α
h : t = ⊤
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
subst h
ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
U : Opens α
this : TopologicalSpace α := ⊤
⊢ U = ⊥ ∨ U = ⊤
ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
letI : TopologicalSpace α := ⊤
ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
U : Opens α
this : TopologicalSpace α := ⊤
⊢ IsOpen ↑U
ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
U : Opens α
this : TopologicalSpace α := ⊤
⊢ U = ⊥ ∨ U = ⊤
rw [← coe_eq_empty, ← coe_eq_univ, ← isOpen_top_iff]
no goals
ι : Type ?u.28720
α✝ : Type ?u.28723
β : Type ?u.28726
γ : Type ?u.28729
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_1
U : Opens α
this : TopologicalSpace α := ⊤
⊢ IsOpen ↑U
exact U.2