Theorem: Tutorial.adjunction.compose (LCTutorial/Exercises/Topics/GaloisAdjunctions.lean)

State before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
⊢ adjunction (l' ∘ l) (r ∘ r')
Tactic:
sorry
State after:
no goals