Decidability of < when constructing LinearOrder via lift'

Stream: mathlib4

[Jure Taslak (Slovenia)]

We have the following example:

import Mathlib.Data.Prod.Lex

structure Pair : Type :=
  (pair : Lex (Nat × Nat))

instance PairLinearOrder : LinearOrder Pair :=
  LinearOrder.lift' (fun (u : Pair) => u.pair) (fun u v H => by cases u; cases v; simp; assumption)

instance comparePairDecidable (p1 p2 : Pair) : Decidable (p1 < p2) := by
  have l : LinearOrder Pair := by apply PairLinearOrder
  have q := l.decidable_lt p1 p2
  simp at q
  exact q

Lean complains that the types don't match via the amusing error message:

type mismatch
  q
has type
  Decidable (p1 < p2) : Type
but is expected to have type
  Decidable (p1 < p2) : Type

If we set set_option pp.explicit true we can see that the types don't match exactly, note @SemilatticeInf.toPartialOrder vs @LinearOrder.toPartialOrder in

type mismatch
  q
has type
  Decidable
    (@LT.lt Pair (@Preorder.toLT Pair (@PartialOrder.toPreorder Pair (@LinearOrder.toPartialOrder Pair l))) p1
      p2) : Type
but is expected to have type
  Decidable
    (@LT.lt Pair
      (@Preorder.toLT Pair
        (@PartialOrder.toPreorder Pair
          (@SemilatticeInf.toPartialOrder Pair
            (@Lattice.toSemilatticeInf Pair
              (@DistribLattice.toLattice Pair (@instDistribLattice Pair PairLinearOrder))))))
      p1 p2) : Type

with the former coming from the definition of LinearOrder and the latter coming from LinearOrder.lift'.

Is there something we can do here?

[Eric Wieser]

have means "create this instance and forget everything"

[Eric Wieser]

Use let:

instance comparePairDecidable (p1 p2 : Pair) : Decidable (p1 < p2) := by
  let l : LinearOrder Pair := by apply PairLinearOrder
  have q := l.decidable_lt p1 p2
  simp at q
  exact q

[Eric Wieser]

But note that you don't need to do anything at all:

-- lean already knows where the instance is
instance comparePairDecidable (p1 p2 : Pair) : Decidable (p1 < p2) := by infer_instance

[Jure Taslak (Slovenia)]

Ah yes of course, infer_instanceis exactly what I was looking for. @Eric Wieser thank you very much.