exact hXZ.compose hZW
case A₁
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
⊢ ?m.150838
no goals