From 5db91116bbd754e937aa4a808597dd8936b320cb Mon Sep 17 00:00:00 2001
From: Paul Reichert <datokrat@users.noreply.github.com>
Date: Wed, 29 Jan 2025 14:39:29 +0100
Subject: [PATCH] fix(failing build): remove now-unneeded tactics after
 nonterminal simp (#1102)

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
---
 Batteries/Classes/Order.lean     | 23 -----------------------
 Batteries/Data/RBMap/Lemmas.lean |  2 +-
 2 files changed, 1 insertion(+), 24 deletions(-)

diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean
index 1296bd7a9d..422025b746 100644
--- a/Batteries/Classes/Order.lean
+++ b/Batteries/Classes/Order.lean
@@ -5,29 +5,6 @@ Authors: Mario Carneiro
 -/
 import Batteries.Tactic.SeqFocus
 
-/-! ## Ordering -/
-
-namespace Ordering
-
-@[simp] theorem swap_swap {o : Ordering} : o.swap.swap = o := by cases o <;> rfl
-
-@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
-  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩
-
-theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap := by
-  cases o₁ <;> rfl
-
-theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by
-  cases o₁ <;> simp [«then»]
-
-theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-end Ordering
-
 namespace Batteries
 
 /-- `TotalBLE le` asserts that `le` has a total order, that is, `le a b ∨ le b a`. -/
diff --git a/Batteries/Data/RBMap/Lemmas.lean b/Batteries/Data/RBMap/Lemmas.lean
index df9ec1d585..b32beaf675 100644
--- a/Batteries/Data/RBMap/Lemmas.lean
+++ b/Batteries/Data/RBMap/Lemmas.lean
@@ -288,7 +288,7 @@ theorem size_eq {t : RBNode α} : t.size = t.toList.length := by
 @[simp] theorem Any_reverse {t : RBNode α} : t.reverse.Any p ↔ t.Any p := by simp [Any_def]
 
 @[simp] theorem memP_reverse {t : RBNode α} : MemP cut t.reverse ↔ MemP (cut · |>.swap) t := by
-  simp [MemP]; apply Iff.of_eq; congr; funext x; rw [← Ordering.swap_inj]; rfl
+  simp [MemP]
 
 theorem Mem_reverse [@OrientedCmp α cmp] {t : RBNode α} :
     Mem cmp x t.reverse ↔ Mem (flip cmp) x t := by