Theorem: Tutorial.push_Sup (LCTutorial/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
⊢ Topology.isOpen (f⁎ (Sup t)) V ↔ Topology.isOpen (Sup (f⁎ '' t)) V

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

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