Decidability on subtypes

Stream: general

[Yaël Dillies]

In #13089 I'm adding

instance subtype.decidable_le [preorder α] [@decidable_rel α (≤)] {p : α → Prop} :
  @decidable_rel (subtype p) (≤) :=
λ a b, decidable_of_iff _ subtype.coe_le_coe

instance subtype.decidable_lt [preorder α] [@decidable_rel α (<)] {p : α → Prop} :
  @decidable_rel (subtype p) (<) :=
λ a b, decidable_of_iff _ subtype.coe_lt_coe

This breaks stuff because we also have

instance subtype.linear_order {α} [linear_order α] (p : α → Prop) : linear_order (subtype p) :=
{ decidable_eq := subtype.decidable_eq,
  .. linear_order.lift coe subtype.coe_injective }

which derives decidability differently. Is it okay if I simply turn this last one into

instance subtype.linear_order {α} [linear_order α] (p : α → Prop) : linear_order (subtype p) :=
{ decidable_eq := subtype.decidable_eq,
  decidable_le := subtype.decidable_le,
  decidable_lt := subtype.decidable_lt,
  .. linear_order.lift coe subtype.coe_injective }

[Yaël Dillies]

Note that the max_def/min_def fields fail, but I can fix those easily.

[Floris van Doorn]

Yeah, it's fine to change that.
This is exactly the reason why the decidable_eq field was given explicitly: to make other decidable proofs definitionally equal.