Theorem: Tutorial.push_Sup (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

State before:
X Y : Type
f : X → Y
t : Set (Topology X)
⊢ f⁎ (Sup t) = Sup (f⁎ '' t)
Tactic:
ext V
State after:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ (Sup (f⁎ '' t)).isOpen V

State before:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ (Sup (f⁎ '' t)).isOpen V
Tactic:
rw [isOpen_Sup, Set.forall_mem_image]
State after:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ ∀ ⦃x : Topology X⦄, x ∈ t → (f⁎ x).isOpen V

State before:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ ∀ ⦃x : Topology X⦄, x ∈ t → (f⁎ x).isOpen V
Tactic:
exact Iff.rfl
State after:
no goals