From f96a8aaf795d50bb08d0f77d452980ef4d918f3e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 31 Jul 2024 15:37:43 +1000
Subject: [PATCH] chore: backports for leanprover/lean4#4814 (#894)

---
 Batteries/Classes/Order.lean    | 2 +-
 Batteries/Data/List/Lemmas.lean | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean
index f54f82eb24..8cbfae25b0 100644
--- a/Batteries/Classes/Order.lean
+++ b/Batteries/Classes/Order.lean
@@ -102,7 +102,7 @@ theorem cmp_congr_left (xy : cmp x y = .eq) : cmp x z = cmp y z :=
 theorem cmp_congr_left' (xy : cmp x y = .eq) : cmp x = cmp y :=
   funext fun _ => cmp_congr_left xy
 
-theorem cmp_congr_right [TransCmp cmp] (yz : cmp y z = .eq) : cmp x y = cmp x z := by
+theorem cmp_congr_right (yz : cmp y z = .eq) : cmp x y = cmp x z := by
   rw [← Ordering.swap_inj, symm, symm, cmp_congr_left yz]
 
 end TransCmp
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index b932b5ff71..533a140f45 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -912,7 +912,7 @@ section union
 
 variable [BEq α]
 
-theorem union_def [BEq α] (l₁ l₂ : List α)  : l₁ ∪ l₂ = foldr .insert l₂ l₁ := rfl
+theorem union_def (l₁ l₂ : List α)  : l₁ ∪ l₂ = foldr .insert l₂ l₁ := rfl
 
 @[simp] theorem nil_union (l : List α) : nil ∪ l = l := by simp [List.union_def, foldr]
 
@@ -977,10 +977,11 @@ theorem forIn_eq_bindList [Monad m] [LawfulMonad m]
 
 section Diff
 variable [BEq α]
-variable [LawfulBEq α]
 
 @[simp] theorem diff_nil (l : List α) : l.diff [] = l := rfl
 
+variable [LawfulBEq α]
+
 @[simp] theorem diff_cons (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.erase a).diff l₂ := by
   simp_all [List.diff, erase_of_not_mem]