From 527b760faddf08a03e5e502f9a15c9b2cd7ad3fa Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 28 Jan 2025 16:02:42 +0100
Subject: [PATCH] derive LawfulBEq

---
 src/Init/Data/Ord.lean | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 5a7c0a149895..b3ae3e9a8c9b 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -10,17 +10,10 @@ import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
-deriving Inhabited, BEq
+deriving Inhabited, DecidableEq
 
 namespace Ordering
 
-deriving instance DecidableEq for Ordering
-
--- This becomes obsolete with https://github.com/leanprover/lean4/issues/5295
-instance : LawfulBEq Ordering where
-  eq_of_beq {a b} := by cases a <;> cases b <;> simp <;> rfl
-  rfl {a} := by cases a <;> rfl
-
 /-- Swaps less and greater ordering results -/
 def swap : Ordering → Ordering
   | .lt => .gt