∀ {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),
  Function.LeftInverse (fun f => CategoryTheory.homOfLE ⋯) fun f => CategoryTheory.homOfLE ⋯