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

State before:
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
⊢ g⁎ (f⁎ T) = (g ∘ f)⁎ T
Tactic:
ext V
State after:
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ Topology.isOpen (g⁎ (f⁎ T)) V ↔ Topology.isOpen ((g ∘ f)⁎ T) V

State before:
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ Topology.isOpen (g⁎ (f⁎ T)) V ↔ Topology.isOpen ((g ∘ f)⁎ T) V
Tactic:
exact Iff.rfl
State after:
no goals