Conditional LinearOrder

Stream: mathlib4

[Moritz R]

Im currently proving some stuff about the DershowitzManna ordering extension
which extends an ordering on a to an ordering on Multiset a.
This extension has lots of nice properties in the sense that it transfers many properties from the order on a to the extension.
E.g. from Preorder a one getsPartialorder (Multiset a)
and from LinearOrder a one gets LinearOrder (Multiset a).

I'm wondering if im doing the conditional LinearOrder def correctly - the LinearOrder should agree with the partialOrder if it exists.

def Multiset.IsDershowitzMannaLT.instPartialOrder [Preorder α] : PartialOrder (Multiset α) :=
  @partialOrderOfSO _ Multiset.IsDershowitzMannaLT Multiset.IsDershowitzMannaLT.IsStrictOrder

def Multiset.IsDershowitzMannaLT.instLinearOrder [LinearOrder α] : LinearOrder (Multiset α) where
  toPartialOrder := @Multiset.IsDershowitzMannaLT.instPartialOrder α _
  toDecidableLE := (@linearOrderOfSTO (Multiset α) Multiset.IsDershowitzMannaLT
    Multiset.IsDershowitzMannaLT.IsStrictTotalOrder _).toDecidableLE
  le_total := (@linearOrderOfSTO _ Multiset.IsDershowitzMannaLT
    Multiset.IsDershowitzMannaLT.IsStrictTotalOrder _).le_total
  min := (@linearOrderOfSTO _ Multiset.IsDershowitzMannaLT
    Multiset.IsDershowitzMannaLT.IsStrictTotalOrder _).min
  max := (@linearOrderOfSTO _ Multiset.IsDershowitzMannaLT
    Multiset.IsDershowitzMannaLT.IsStrictTotalOrder _).max

[Moritz R]

And one additional question:
I later need to pull back both of these defs via an injective function.
Can i just do the following (or will this get me any diamonds?)

/-- Literals are compared, by comparing `L1.toMultiset` and `L2.toMultiset` using
    the multiset extension. -/
instance (priority := high) Literal.instPartialOrder [PartialOrder (Term F α)] :
    PartialOrder (Literal F α) :=
  @PartialOrder.lift _ _
    Multiset.IsDershowitzMannaLT.instPartialOrder
    Literal.toMultiset
    Literal.toMultiset_injective

/-- Literals are compared, by comparing `L1.toMultiset` and `L2.toMultiset` using
    the multiset extension. -/
instance (priority := high) Literal.instLinearOrder [LinearOrder (Term F α)] :
    LinearOrder (Literal F α) :=
  @LinearOrder.lift' _ _
    Multiset.IsDershowitzMannaLT.instLinearOrder
    Literal.toMultiset
    Literal.toMultiset_injective

[Moritz R]

This should be fine, since both lifts are abbrevs and the orders are in both cases defined using the same condition right?

[Eric Wieser]

You should tag your multiset defs with instance_reducible

[Moritz R]

Can you exlain what that is needed for?

[Moritz R]

Should i always do this with defs that have a class type as the result?

[Eric Wieser]

This is needed so that lean can tell the two instances are the same without having to turn on more aggressive unfolding