Lean comes with a decidable_linear_order typeclass containing useful lemmas about an ordering and its relation to equality, such as:
lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a
The equalities in these orderings are all expressed in terms of =:
inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a
I was wondering whether it would be possible to somehow extend this class (and its superclasses) to work with an arbitrary used defined equality relation R: α → α → Prop that was reflexive, symmetric and transitive, or would this only be possible by rewriting all the relevant lemmas and their proofs to use R instead of eq?
Since these classes are not parameterized by the equality relation, you would indeed have to reimplement them (perhaps metaprogramming may be of help for that). Alternatively, because you have an equivalence relation, you could define your order on the quotient type and so keep using eq.