Antisymm instance

Stream: mathlib4

[Andy Jiang]

Newbie question: Is there a reason in the code

/-- `IsAntisymm X r` means the binary relation `r` on `X` is antisymmetric. -/
class IsAntisymm (α : Type u) (r : α → α → Prop) : Prop where
  antisymm : ∀ a b, r a b → r b a → a = b
#align is_antisymm IsAntisymm

/-- `IsTrans X r` means the binary relation `r` on `X` is transitive. -/
class IsTrans (α : Type u) (r : α → α → Prop) : Prop where
  trans : ∀ a b c, r a b → r b c → r a c
#align is_trans IsTrans

instance {α : Type u} {r : α → α → Prop} [IsTrans α r] : Trans r r r :=
  ⟨IsTrans.trans _ _ _⟩

instance {α : Type u} {r : α → α → Prop} [Trans r r r] : IsTrans α r :=
  ⟨fun _ _ _ => Trans.trans⟩

in mathlib4/Mathlib/Init/Algebra/Classes.lean
there's no instance code for Antisymm but only for trans? I think it prevents some automatic inferences (but maybe I'm mistaken about that). In particular when I tried to use <= for Nat in a function which required both implicitly, Lean inferred the trans but not the antisymm. Thanks in advance!

[Eric Wieser]

Init.Algebra.Classes, as indicated at the top of the file, is mostly junk left from a lean3 refactor that never happened