Theorem: Tutorial.push_push (GlimpseOfLean/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
⊢ (g⁎ (f⁎ T)).isOpen V ↔ ((g ∘ f)⁎ T).isOpen V

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