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

State before:
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
r r' : Y → X
h : adjunction l r
h' : adjunction l r'
⊢ r = r'
Tactic:
exact (unique_left h'.dual h.dual).symm
State after:
no goals