∀ {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : α → β) (g : β → α)
  (h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) (gf : ∀ (a : α), a = g (f a)) {a b : α},
  { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b