Theorem: Tutorial.isOpen_univ (LCTutorial/Solutions/Topics/GaloisAdjunctions.lean)

State before:
X : Type
T : Topology X
⊢ Topology.isOpen T Set.univ
Tactic:
have : (Set.univ : Set X) = ⋂ i : Empty, i.rec
State after:
case this
X : Type
T : Topology X
⊢ Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i

X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T Set.univ

State before:
X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T Set.univ
Tactic:
rw [this]
State after:
X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T (⋂ (i : Empty), Empty.rec (fun x => Set X) i)

State before:
X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T (⋂ (i : Empty), Empty.rec (fun x => Set X) i)
Tactic:
exact T.isOpen_iInter  Empty.rec (Finite.of_fintype Empty)
State after:
no goals

State before:
case this
X : Type
T : Topology X
⊢ Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
Tactic:
rw [Set.iInter_of_empty]
State after:
no goals