∀ {X : Type u_2} {Y : Type u_1} [inst : Preorder X] [inst_1 : Preorder Y] {l : X → Y} {u : Y → X}
  (gc : GaloisConnection l u) {X_1 : X} {Y_1 Y' : Y} (f : ⋯.functor.obj X_1 ⟶ Y_1) (g : Y_1 ⟶ Y'),
  { toFun := fun f => CategoryTheory.homOfLE ⋯, invFun := fun f => CategoryTheory.homOfLE ⋯, left_inv := ⋯,
        right_inv := ⋯ }
      (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      ({ toFun := fun f => CategoryTheory.homOfLE ⋯, invFun := fun f => CategoryTheory.homOfLE ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        f)
      (⋯.functor.map g)