Get is_linear_order

Stream: new members

[Marcus Rossel]

Is there an easy way of removing the following sorry: ?

import data.nat.basic

@[derive has_le, derive has_lt]
def mass := ℕ

@[ext]
structure object :=
  (m : mass)
  (n : ℕ)

instance object_le : has_le object := ⟨λ o o', o.m < o'.m ∨ (o.m = o'.m ∧ o.n ≤ o'.n)⟩

instance object_le_linear : is_linear_order object (≤) := sorry

The object structure is basically just an ℕ × ℕ and its ≤ is lexicographic.
I would like to avoid proving reflexivity, transitivity, antisymmetry and totality manually. Is that possible?

[Heather Macbeth]

docs#lex

[Marcus Rossel]

Unfortunately I need to keep the structure, so I can't just def object := lex mass ℕ.

[Mario Carneiro]

docs#linear_order.lift

[Marcus Rossel]

Mario Carneiro said:

docs#linear_order.lift

I don't understand how to use this. Could you perhaps show an example? :)

[Marcus Rossel]

Is this the intended use?

def object.to_lex (o : object) : lex ℕ ℕ := (o.m, o.n)
instance : linear_order object := linear_order.lift object.to_lex sorry

[Mario Carneiro]

import data.nat.basic order.lexicographic

@[derive linear_order]
def mass := ℕ

@[ext]
structure object :=
  (m : mass)
  (n : ℕ)

instance : linear_order object :=
@linear_order.lift _ (lex mass ℕ) _
  (λ o:object, (o.m, o.n)) (by rintro ⟨⟩ ⟨⟩ ⟨⟩; refl)