chore: cleanup lexOrd_def (#915)

leanprover-community · Aug 14, 2024 · 5e5e54c · 5e5e54c
1 parent 1d25ec7
commit 5e5e54c
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean
@@ -278,11 +278,8 @@ instance [Ord β] [OrientedOrd β] (f : α → β) : OrientedCmp (compareOn f) w
 instance [Ord β] [TransOrd β] (f : α → β) : TransCmp (compareOn f) where
   le_trans := TransCmp.le_trans (α := β)
 
--- FIXME: remove after lean4#3882 is merged
 theorem _root_.lexOrd_def [Ord α] [Ord β] :
-    (lexOrd : Ord (α × β)).compare = compareLex (compareOn (·.1)) (compareOn (·.2)) := by
-  funext a b
-  simp [lexOrd, compareLex, compareOn]
+    (lexOrd : Ord (α × β)).compare = compareLex (compareOn (·.1)) (compareOn (·.2)) := rfl
 
 section «non-canonical instances»
 -- Note: the following instances seem to cause lean to fail, see: