Theorem: Tutorial.isOpen_empty (GlimpseOfLean/Exercises/Topics/GaloisAdjunctions.lean)

State before:
X : Type
T : Topology X
⊢ T.isOpen ∅
Tactic:
have : (∅ : Set X) = ⋃ i : Empty, i.rec := by
  rw [Set.iUnion_of_empty]
State after:
X : Type
T : Topology X
this : ∅ = ⋃ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen ∅

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

State before:
X : Type
T : Topology X
this : ∅ = ⋃ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen (⋃ i, Empty.rec (fun x => Set X) i)
Tactic:
exact T.isOpen_iUnion Empty.rec
State after:
no goals

State before:
X : Type
T : Topology X
⊢ ∅ = ⋃ i, Empty.rec (fun x => Set X) i
Tactic:
rw [Set.iUnion_of_empty]
State after:
no goals