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

State before:
α β : Type
f : α → β
⊢ adjunction (Set.image f) (Set.preimage f)
Tactic:
intros s t
State after:
α β : Type
f : α → β
s : Set α
t : Set β
⊢ f '' s ≤ t ↔ s ≤ f ⁻¹' t

State before:
α β : Type
f : α → β
s : Set α
t : Set β
⊢ f '' s ≤ t ↔ s ≤ f ⁻¹' t
Tactic:
exact Set.image_subset_iff
State after:
no goals