Relclasses instances

Stream: mathlib4

[Sebastien Gouezel]

We have in Order.RelClasses

/-- A well order is a well-founded linear order. -/
class IsWellOrder (α : Type u) (r : α → α → Prop) extends
  IsTrichotomous α r, IsTrans α r, IsWellFounded α r : Prop
#align is_well_order IsWellOrder

-- see Note [lower instance priority]
instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] :
    IsStrictTotalOrder α r where

-- see Note [lower instance priority]
instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsTrichotomous α r := by
  infer_instance

-- see Note [lower instance priority]
instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsTrans α r := by
  infer_instance

-- see Note [lower instance priority]
instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsIrrefl α r := by
  infer_instance

-- see Note [lower instance priority]
instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsAsymm α r := by
  infer_instance

Why are the last 4 instances since they can already be inferred (and are in fact part of the very definition)?

[Eric Wieser]

Was this a porting error?

[Eric Wieser]

I think this might be a failed attempt to lower the priority?