∀ {a b : YoungDiagram},
  { toFun := YoungDiagram.transpose, invFun := YoungDiagram.transpose, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := YoungDiagram.transpose, invFun := YoungDiagram.transpose, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b