Transfer via concrete OrderIso or class-like OrderIsoClass

Stream: mathlib4

[Yakov Pechersky]

I have two functionally equivalent PRs. I want to transfer SuccOrder across an order isomorphism.

In #15950, I do so using OrderIsoClass.

variable {X Y F : Type*} [EquivLike F X Y] [Preorder X] [Preorder Y] [OrderIsoClass F X Y]

@[reducible] protected def SuccOrder [SuccOrder X] (f : F) : SuccOrder Y where ...

In #16490, I do so using OrderIso.

@[reducible]
def SuccOrder.of_orderIso {X Y : Type*} [Preorder X] [Preorder Y] [SuccOrder X] (f : X ≃o Y) :
    SuccOrder Y where ...

I had closed #16490 because I thought there is a preference for class based lemmas. @Yaël Dillies indicated that the class pattern might be worse. What is the more appropriate solution?

[Yaël Dillies]

Sorry, I think you misunderstood my comment. What I meant to say is that the following looks like a bad idea:

instance (priority := 100) OrderIsoClass.toOrderIsoClassOrderDual [LE α] [LE β]
    [EquivLike F α β] [OrderIsoClass F α β] : OrderIsoClass F αᵒᵈ βᵒᵈ where
  map_le_map_iff f := map_le_map_iff f

[Yakov Pechersky]

I see. Still, to transfer PredOrder, I'd like to work through a dualized setup, so something of that instance would be necessary. I could make it an explicit def, or rely on concrete OrderIsos in total.