∀ {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : γ →o δ),
  (↑g).comp (((↑g.symm).comp (p.comp ↑f)).comp ↑f.symm) = p