From c379a531de82be5c6cead470995522728b5b4383 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 31 Jan 2025 22:06:40 +1100
Subject: [PATCH] remove upstreamed

---
 Batteries/Classes/Order.lean     |  23 ------
 Batteries/Data/Array/Lemmas.lean | 122 -------------------------------
 2 files changed, 145 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/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index dfd5198d1c..08fdf6679d 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -32,132 +32,10 @@ theorem forIn_eq_forIn_toList [Monad m]
 @[deprecated (since := "2024-08-13")] alias join_data := toList_flatten
 @[deprecated (since := "2024-10-15")] alias mem_join := mem_flatten
 
-end Array
-
 /-! ### indexOf? -/
 
-namespace Array
-
-theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} :
-    findIdx?.loop p xs j = (findFinIdx?.loop p xs j).map (·.val) := by
-  unfold findIdx?.loop
-  unfold findFinIdx?.loop
-  split <;> rename_i h
-  case isTrue =>
-    split
-    case isTrue => simp
-    case isFalse =>
-      have : xs.size - (j + 1) < xs.size - j := Nat.sub_succ_lt_self xs.size j h
-      rw [findIdx?_loop_eq_map_findFinIdx?_loop_val (j := j + 1)]
-  case isFalse => simp
-termination_by xs.size - j
-
-theorem findIdx?_eq_map_findFinIdx?_val {xs : Array α} {p : α → Bool} :
-    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
-  simp [findIdx?, findFinIdx?, findIdx?_loop_eq_map_findFinIdx?_loop_val]
-
-end Array
-
-namespace List
-
-theorem findFinIdx?_go_beq_eq_idxOfAux_toArray [BEq α]
-    {xs as : List α} {a : α} {i : Nat} {h} (w : as = xs.drop i) :
-    findFinIdx?.go (fun x => x == a) xs as i h =
-      xs.toArray.idxOfAux a i := by
-  unfold findFinIdx?.go
-  unfold Array.idxOfAux
-  split <;> rename_i b as
-  · simp at h
-    simp [h]
-  · simp at h
-    rw [dif_pos (by simp; omega)]
-    simp only [getElem_toArray]
-    erw [getElem_drop' (j := 0)]
-    simp only [← w, getElem_cons_zero]
-    have : xs.length - (i + 1) < xs.length - i := by omega
-    rw [findFinIdx?_go_beq_eq_idxOfAux_toArray]
-    rw [← drop_drop, ← w]
-    simp
-termination_by xs.length - i
-
-@[simp] theorem finIdxOf?_toArray [BEq α] {as : List α} {a : α} :
-    as.toArray.finIdxOf? a = as.finIdxOf? a := by
-  unfold Array.finIdxOf?
-  unfold finIdxOf?
-  unfold findFinIdx?
-  rw [findFinIdx?_go_beq_eq_idxOfAux_toArray]
-  simp
-
-theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
-    List.findIdx?.go p xs i =
-      (List.findFinIdx?.go p l xs i h).map (·.val) := by
-  unfold findIdx?.go
-  unfold findFinIdx?.go
-  split <;> rename_i a xs
-  · simp_all
-  · simp only
-    split
-    · simp
-    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
-  simp [findIdx?, findFinIdx?]
-  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
-    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
-  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
-
-@[simp] theorem idxOf?_toArray [BEq α] {as : List α} {a : α} :
-    as.toArray.idxOf? a = as.idxOf? a := by
-  rw [Array.idxOf?, finIdxOf?_toArray, idxOf?_eq_map_finIdxOf?_val]
-
-open Array in
-@[simp] theorem findIdx?_toArray {as : List α} {p : α → Bool} :
-    as.toArray.findIdx? p = as.findIdx? p := by
-  unfold Array.findIdx?
-  suffices ∀ i, i ≤ as.length →
-      Array.findIdx?.loop p as.toArray (as.length - i) =
-        (findIdx? p (as.drop  (as.length - i))).map fun j => j +  (as.length - i) by
-    specialize this as.length
-    simpa
-  intro i
-  induction i with
-  | zero => simp [findIdx?.loop]
-  | succ i ih =>
-    unfold findIdx?.loop
-    simp only [size_toArray, getElem_toArray]
-    split <;> rename_i h
-    · rw [drop_eq_getElem_cons h]
-      rw [findIdx?_cons]
-      split <;> rename_i h'
-      · simp
-      · intro w
-        have : as.length - (i + 1) + 1 = as.length - i := by omega
-        specialize ih (by omega)
-        simp only [Option.map_map, this, ih]
-        congr
-        ext
-        simp
-        omega
-    · have : as.length = 0 := by omega
-      simp_all
-
-@[simp] theorem findFinIdx?_toArray {as : List α} {p : α → Bool} :
-    as.toArray.findFinIdx? p = as.findFinIdx? p := by
-  have h := findIdx?_toArray (as := as) (p := p)
-  rw [findIdx?_eq_map_findFinIdx?_val, Array.findIdx?_eq_map_findFinIdx?_val] at h
-  rwa [Option.map_inj_right] at h
-  rintro ⟨x, hx⟩ ⟨y, hy⟩ rfl
-  simp
-
-end List
-
 open List
 
-namespace Array
-
 theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
     l.toList.idxOf? a = l.idxOf? a := by
   rcases l with ⟨l⟩