cleanup

src/Init/Data/Array.lean

@@ -15,4 +15,3 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
-import Init.Data.Array.GetLit

src/Init/Data/Array/Basic.lean

@@ -13,76 +13,43 @@ import Init.Data.ToString.Basic
 import Init.GetElem
 universe u v w
 
-/-! ### Array literal syntax -/
-
-syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
-
-macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
-
-variable {α : Type u}
-
 namespace Array
-
-/-! ### Preliminary theorems -/
-
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
-  List.length_set ..
-
-@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
-  List.length_concat ..
-
-theorem ext (a b : Array α)
-    (h₁ : a.size = b.size)
-    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
-    : a = b := by
-  let rec extAux (a b : List α)
-      (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
-      : a = b := by
-    induction a generalizing b with
-    | nil =>
-      cases b with
-      | nil       => rfl
-      | cons b bs => rw [List.length_cons] at h₁; injection h₁
-    | cons a as ih =>
-      cases b with
-      | nil => rw [List.length_cons] at h₁; injection h₁
-      | cons b bs =>
-        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have headEq : a = b := h₂ 0 hz₁ hz₂
-        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
-          intro i hi₁ hi₂
-          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
-          apply this
-        have tailEq : as = bs := ih bs h₁' h₂'
-        rw [headEq, tailEq]
-  cases a; cases b
-  apply congrArg
-  apply extAux
-  assumption
-  assumption
-
-theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
-  cases as; cases bs; simp at h; rw [h]
-
-@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
-  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
-
-@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
-  simp [List.toArray, Array.mkEmpty]
-
-@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
-
-@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+variable {α : Type u}
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
 
-/-! ### Externs -/
+@[extern "lean_mk_array"]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
+/--
+`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
+```
+ofFn f = #[f 0, f 1, ... , f(n - 1)]
+``` -/
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
+  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
+  go (i : Nat) (acc : Array α) : Array α :=
+    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
+termination_by n - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) (mkEmpty n)
+
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
+instance : EmptyCollection (Array α) := ⟨Array.empty⟩
+instance : Inhabited (Array α) where
+  default := Array.empty
+
+@[simp] def isEmpty (a : Array α) : Bool :=
+  a.size = 0
+
+def singleton (v : α) : Array α :=
+  mkArray 1 v
 
 /-- Low-level version of `size` that directly queries the C array object cached size.
     While this is not provable, `usize` always returns the exact size of the array since
@@ -98,6 +65,29 @@ def usize (a : @& Array α) : USize := a.size.toUSize
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
+instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+  getElem xs i h := xs.uget i h
+
+def back [Inhabited α] (a : Array α) : α :=
+  a.get! (a.size - 1)
+
+def get? (a : Array α) (i : Nat) : Option α :=
+  if h : i < a.size then some a[i] else none
+
+def back? (a : Array α) : Option α :=
+  a.get? (a.size - 1)
+
+-- auxiliary declaration used in the equation compiler when pattern matching array literals.
+abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
+  have := h₁.symm ▸ h₂
+  a[i]
+
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+  List.length_set ..
+
+@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
+  List.length_concat ..
+
 /-- Low-level version of `fset` which is as fast as a C array fset.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fset` may be slightly slower than `uset`. -/
@@ -105,19 +95,6 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
-@[extern "lean_array_pop"]
-def pop (a : Array α) : Array α where
-  toList := a.toList.dropLast
-
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
-  match a with
-  | ⟨[]⟩ => rfl
-  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
-
-@[extern "lean_mk_array"]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
-  toList := List.replicate n v
-
 /--
 Swaps two entries in an array.
 
@@ -131,10 +108,6 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let a'  := a.set i v₂
   a'.set (size_set a i v₂ ▸ j) v₁
 
-@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
-  rw [size_set, size_set]
-
 /--
 Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
@@ -148,66 +121,6 @@ def swap! (a : Array α) (i j : @& Nat) : Array α :=
   else a
   else a
 
-/-! ### GetElem instance for `USize`, backed by `uget` -/
-
-instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-  getElem xs i h := xs.uget i h
-
-/-! ### Definitions -/
-
-instance : EmptyCollection (Array α) := ⟨Array.empty⟩
-instance : Inhabited (Array α) where
-  default := Array.empty
-
-@[simp] def isEmpty (a : Array α) : Bool :=
-  a.size = 0
-
--- TODO(Leo): cleanup
-@[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
-  if h : i < a.size then
-     have : i < b.size := hsz ▸ h
-     p a[i] b[i] && isEqvAux a b hsz p (i+1)
-  else
-    true
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
-  if h : a.size = b.size then
-    isEqvAux a b h p 0
-  else
-    false
-
-instance [BEq α] : BEq (Array α) :=
-  ⟨fun a b => isEqv a b BEq.beq⟩
-
-/--
-`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
-```
-ofFn f = #[f 0, f 1, ... , f(n - 1)]
-``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
-def singleton (v : α) : Array α :=
-  mkArray 1 v
-
-def back [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
-
-def get? (a : Array α) (i : Nat) : Option α :=
-  if h : i < a.size then some a[i] else none
-
-def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
-
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a.get i
   let a := a.set i v
@@ -221,6 +134,10 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited α := ⟨v⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
+@[extern "lean_array_pop"]
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
+
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
@@ -394,6 +311,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
       map (i+1) (r.push (← f as[i]))
     else
       pure r
+  termination_by as.size - i
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -466,6 +384,7 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
+      termination_by stop - j
       decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
@@ -551,22 +470,12 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
+    termination_by as.size - j
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-  a.findIdx? fun a => a == v
-
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
-  if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
-    else indexOfAux a v (i+1)
-  else none
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
+a.findIdx? fun a => a == v
 
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
@@ -582,6 +491,13 @@ def contains [BEq α] (as : Array α) (a : α) : Bool :=
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
 
+@[inline] def getEvenElems (as : Array α) : Array α :=
+  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
+    if even then
+      (false, r.push a)
+    else
+      (true, r)
+
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
 -- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
@@ -594,6 +510,17 @@ def toListImpl (as : Array α) : List α :=
 def toListAppend (as : Array α) (l : List α) : List α :=
   as.foldr List.cons l
 
+instance {α : Type u} [Repr α] : Repr (Array α) where
+  reprPrec a _ :=
+    let _ : Std.ToFormat α := ⟨repr⟩
+    if a.size == 0 then
+      "#[]"
+    else
+      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
+
+instance [ToString α] : ToString (Array α) where
+  toString a := "#" ++ toString a.toList
+
 protected def append (as : Array α) (bs : Array α) : Array α :=
   bs.foldl (init := as) fun r v => r.push v
 
@@ -619,13 +546,44 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
 def flatten (as : Array (Array α)) : Array α :=
   as.foldl (init := empty) fun r a => r ++ a
 
+end Array
+
+export Array (mkArray)
+
+syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
+
+macro_rules
+  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+
+namespace Array
+
+-- TODO(Leo): cleanup
+@[specialize]
+def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
+  if h : i < a.size then
+     have : i < b.size := hsz ▸ h
+     p a[i] b[i] && isEqvAux a b hsz p (i+1)
+  else
+    true
+termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
+  if h : a.size = b.size then
+    isEqvAux a b h p 0
+  else
+    false
+
+instance [BEq α] : BEq (Array α) :=
+  ⟨fun a b => isEqv a b BEq.beq⟩
+
 @[inline]
 def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
   as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>
     if p a then r.push a else r
 
 @[inline]
-def filterM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
+def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
   as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
     if (← p a) then return r.push a else return r
 
@@ -660,23 +618,92 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
       cs := cs.push a
   return (bs, cs)
 
+theorem ext (a b : Array α)
+    (h₁ : a.size = b.size)
+    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
+    : a = b := by
+  let rec extAux (a b : List α)
+      (h₁ : a.length = b.length)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
+      : a = b := by
+    induction a generalizing b with
+    | nil =>
+      cases b with
+      | nil       => rfl
+      | cons b bs => rw [List.length_cons] at h₁; injection h₁
+    | cons a as ih =>
+      cases b with
+      | nil => rw [List.length_cons] at h₁; injection h₁
+      | cons b bs =>
+        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have headEq : a = b := h₂ 0 hz₁ hz₂
+        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
+          intro i hi₁ hi₂
+          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
+          apply this
+        have tailEq : as = bs := ih bs h₁' h₂'
+        rw [headEq, tailEq]
+  cases a; cases b
+  apply congrArg
+  apply extAux
+  assumption
+  assumption
+
+theorem extLit {n : Nat}
+    (a b : Array α)
+    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
+    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
+  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
+
+end Array
+
+-- CLEANUP the following code
+namespace Array
+
+def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+  if h : i < a.size then
+    let idx : Fin a.size := ⟨i, h⟩;
+    if a.get idx == v then some idx
+    else indexOfAux a v (i+1)
+  else none
+termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  indexOfAux a v 0
+
+@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  rw [size_set, size_set]
+
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
+
+theorem reverse.termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
+  rw [Nat.sub_sub, Nat.add_comm]
+  exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
+
 def reverse (as : Array α) : Array α :=
   if h : as.size ≤ 1 then
     as
   else
     loop as 0 ⟨as.size - 1, Nat.pred_lt (mt (fun h : as.size = 0 => h ▸ by decide) h)⟩
 where
-  termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
-    rw [Nat.sub_sub, Nat.add_comm]
-    exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
   loop (as : Array α) (i : Nat) (j : Fin as.size) :=
     if h : i < j then
-      have := termination h
+      have := reverse.termination h
       let as := as.swap ⟨i, Nat.lt_trans h j.2⟩ j
       have : j-1 < as.size := by rw [size_swap]; exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
       loop as (i+1) ⟨j-1, this⟩
     else
       as
+termination_by j - i
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
@@ -686,6 +713,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
+termination_by as.size
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
@@ -698,6 +726,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
+    termination_by as.size - i
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
@@ -715,7 +744,6 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
 termination_by a.size - i.val
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
--- This is required in `Lean.Data.PersistentHashMap`.
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ ih =>
@@ -746,6 +774,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
+    termination_by j.1
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
@@ -757,6 +786,41 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
+def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
+  | 0,     _,  acc => acc
+  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
+
+def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
+  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
+
+theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
+  cases as; cases bs; simp at h; rw [h]
+
+@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
+  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
+
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
+  simp [List.toArray, Array.mkEmpty]
+
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+
+theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
+  apply ext'
+  simp [toArrayLit, toList_toArray]
+  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
+  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
+  have := go n hle
+  rw [List.drop_eq_nil_of_le hge] at this
+  rw [this]
+where
+  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
+    rfl
+
+  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
+    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
+
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -768,6 +832,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
+termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
@@ -778,6 +843,23 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
+private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
+  | 0,   _ => true
+  | i+1, h =>
+    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
+    a != as[i] && allDiffAuxAux as a i this
+
+private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
+  if h : i < as.size then
+    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
+  else
+    true
+termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def allDiff [BEq α] (as : Array α) : Bool :=
+  allDiffAux as 0
+
 @[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
@@ -788,6 +870,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
       cs
   else
     cs
+termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
@@ -803,47 +886,4 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
-/-! ### Auxiliary functions used in metaprogramming.
-
-We do not intend to provide verification theorems for these functions.
--/
-
-private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
-  | 0,   _ => true
-  | i+1, h =>
-    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
-    a != as[i] && allDiffAuxAux as a i this
-
-private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
-  if h : i < as.size then
-    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
-  else
-    true
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def allDiff [BEq α] (as : Array α) : Bool :=
-  allDiffAux as 0
-
-@[inline] def getEvenElems (as : Array α) : Array α :=
-  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
-    if even then
-      (false, r.push a)
-    else
-      (true, r)
-
-/-! ### Repr and ToString -/
-
-instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec a _ :=
-    let _ : Std.ToFormat α := ⟨repr⟩
-    if a.size == 0 then
-      "#[]"
-    else
-      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
-
-instance [ToString α] : ToString (Array α) where
-  toString a := "#" ++ toString a.toList
-
 end Array
-
-export Array (mkArray)

src/Init/Data/Array/GetLit.lean

@@ -1,46 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-
-prelude
-import Init.Data.Array.Basic
-
-namespace Array
-
-/-! ### getLit -/
-
--- auxiliary declaration used in the equation compiler when pattern matching array literals.
-abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
-  have := h₁.symm ▸ h₂
-  a[i]
-
-theorem extLit {n : Nat}
-    (a b : Array α)
-    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
-    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
-  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
-
-def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
-  | 0,     _,  acc => acc
-  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
-
-def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
-  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
-
-theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
-  apply ext'
-  simp [toArrayLit, toList_toArray]
-  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
-  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
-  have := go n hle
-  rw [List.drop_eq_nil_of_le hge] at this
-  rw [this]
-where
-  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
-    rfl
-  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
-
-end Array

src/Init/Data/Array/Lemmas.lean

@@ -271,9 +271,6 @@ termination_by n - i
 
 /-- # mkArray -/
 
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
 @[deprecated toList_mkArray (since := "2024-09-09")]
@@ -498,6 +495,7 @@ abbrev size_eq_length_data := @size_eq_length_toList
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
     rw [reverse.loop]
     if h : i < j then
+      have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
     termination_by j - i
@@ -529,8 +527,9 @@ set_option linter.deprecated false in
       (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
       (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
-    · match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel]
+    · have p := reverse.termination h₁
+      match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel] at p ⊢
       rw [(go · (i+1) j)]
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
@@ -1114,4 +1113,5 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
+
 end Array

src/Init/Data/List/Erase.lean

@@ -109,10 +109,6 @@ protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP
 theorem length_eraseP_le (l : List α) : (l.eraseP p).length ≤ l.length :=
   l.eraseP_sublist.length_le
 
-theorem le_length_eraseP (l : List α) : l.length - 1 ≤ (l.eraseP p).length := by
-  rw [length_eraseP]
-  split <;> simp
-
 theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset _ ·)
 
 @[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
@@ -336,10 +332,6 @@ theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁
 theorem length_erase_le (a : α) (l : List α) : (l.erase a).length ≤ l.length :=
   (erase_sublist a l).length_le
 
-theorem le_length_erase [LawfulBEq α] (a : α) (l : List α) : l.length - 1 ≤ (l.erase a).length := by
-  rw [length_erase]
-  split <;> simp
-
 theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset _ _ h
 
 @[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
@@ -460,22 +452,13 @@ end erase
 
 /-! ### eraseIdx -/
 
-theorem length_eraseIdx (l : List α) (i : Nat) :
-    (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length := by
-  induction l generalizing i with
-  | nil => simp
-  | cons x l ih =>
-    cases i with
-    | zero => simp
-    | succ i =>
-      simp only [eraseIdx, length_cons, ih, add_one_lt_add_one_iff, Nat.add_one_sub_one]
-      split
-      · cases l <;> simp_all
-      · rfl
-
-theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
-    (l.eraseIdx i).length = length l - 1 := by
-  simp [length_eraseIdx, h]
+theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i) = length l - 1
+  | [], _, _ => rfl
+  | _::_, 0, _ => by simp [eraseIdx]
+  | x::xs, i+1, h => by
+    have : i < length xs := Nat.lt_of_succ_lt_succ h
+    simp [eraseIdx, ← Nat.add_one]
+    rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
 
 @[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
 
@@ -485,8 +468,6 @@ theorem eraseIdx_eq_take_drop_succ :
   | a::l, 0 => by simp
   | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
 
--- See `Init.Data.List.Nat.Erase` for `getElem?_eraseIdx` and `getElem_eraseIdx`.
-
 @[simp] theorem eraseIdx_eq_nil {l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0) := by
   match l, i with
   | [], _
@@ -518,13 +499,6 @@ theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ len
 theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l := by
   rw [eraseIdx_eq_self.2 h]
 
-theorem length_eraseIdx_le (l : List α) (i : Nat) : length (l.eraseIdx i) ≤ length l :=
-  (eraseIdx_sublist l i).length_le
-
-theorem le_length_eraseIdx (l : List α) (i : Nat) : length l - 1 ≤ length (l.eraseIdx i) := by
-  rw [length_eraseIdx]
-  split <;> simp
-
 theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
     eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
   induction l generalizing k with
@@ -546,7 +520,7 @@ theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤
 theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
     (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a := by
   split <;> rename_i h
-  · rw [eq_replicate_iff, length_eraseIdx_of_lt (by simpa using h)]
+  · rw [eq_replicate_iff, length_eraseIdx (by simpa using h)]
     simp only [length_replicate, true_and]
     intro b m
     replace m := mem_of_mem_eraseIdx m

src/Init/Data/List/Find.lean

@@ -620,18 +620,6 @@ theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α
   · rfl
   · simp_all
 
-theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [findIdx_cons, cond_eq_if]
-    split
-    · simp
-    · split
-      · simp_all
-      · simp only [Nat.add_le_add_iff_right]
-        exact ih fun _ m w => h _ (mem_cons_of_mem x m) w
-
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
@@ -815,7 +803,7 @@ theorem findIdx?_join {l : List (List α)} {p : α → Bool} :
     simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
     split <;> simp_all
 
-theorem findIdx?_eq_findSome?_enum {xs : List α} {p : α → Bool} :
+theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
     xs.findIdx? p = xs.enum.findSome? fun ⟨i, a⟩ => if p a then some i else none := by
   induction xs with
   | nil => simp
@@ -826,30 +814,6 @@ theorem findIdx?_eq_findSome?_enum {xs : List α} {p : α → Bool} :
     · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
       simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
 
-theorem findIdx?_eq_fst_find?_enum {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = (xs.enum.find? fun ⟨_, x⟩ => p x).map (·.1) := by
-  induction xs with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, enum_cons]
-    split
-    · simp_all
-    · simp only [Option.map_map, enumFrom_eq_map_enum, Bool.false_eq_true, not_false_eq_true,
-        find?_cons_of_neg, find?_map, *]
-      congr
-
--- See also `findIdx_le_findIdx`.
-theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :
-    xs.findIdx? q = none → xs.findIdx? p = none := by
-  simp only [findIdx?_eq_none_iff]
-  intro h x m
-  cases z : p x
-  · rfl
-  · exfalso
-    specialize w x m z
-    specialize h x m
-    simp_all
-
 theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome := by
   simp only [List.findIdx?_isSome, any_eq_true]

src/Init/Data/List/Lemmas.lean

@@ -266,15 +266,9 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
 theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
   simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
 
-theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
-  rw [eq_comm, getElem?_eq_some_iff]
-
 @[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
   simp only [← get?_eq_getElem?, get?_eq_none]
 
-@[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? ↔ length l ≤ n := by
-  simp [eq_comm (a := none)]
-
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
 theorem getElem?_eq (l : List α) (i : Nat) :

src/Init/Data/List/Nat.lean

@@ -10,5 +10,3 @@ import Init.Data.List.Nat.Range
 import Init.Data.List.Nat.Sublist
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Count
-import Init.Data.List.Nat.Erase
-import Init.Data.List.Nat.Find

src/Init/Data/List/Nat/Basic.lean

@@ -5,7 +5,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Count
-import Init.Data.List.Find
 import Init.Data.List.MinMax
 import Init.Data.Nat.Lemmas
 
@@ -119,53 +118,6 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
-theorem foldl_min
-    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
-    {l : List α} {a : α} :
-    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
-  cases l with
-  | nil => simp [Std.IdempotentOp.idempotent]
-  | cons b l =>
-    simp only [minimum?]
-    induction l generalizing a b with
-    | nil => simp
-    | cons c l ih => simp [ih, Std.Associative.assoc]
-
-theorem foldl_min_right {α β : Type _}
-    [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
-    {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
-  rw [← foldl_map, foldl_min]
-
-theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
-  induction l generalizing a with
-  | nil => simp
-  | cons c l ih =>
-    simp only [foldl_cons]
-    exact Nat.le_trans ih (Nat.min_le_left _ _)
-
-theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
-    l.foldl (init := a) min ≤ b :=
-  Nat.le_trans (foldl_min_le) h
-
-theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    l.minimum?.getD k ≤ a := by
-  cases l with
-  | nil => simp at h
-  | cons b l =>
-    simp [minimum?_cons]
-    simp at h
-    rcases h with (rfl | h)
-    · exact foldl_min_le
-    · induction l generalizing b with
-      | nil => simp_all
-      | cons c l ih =>
-        simp only [foldl_cons]
-        simp at h
-        rcases h with (rfl | h)
-        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
-        · exact ih _ h
-
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -199,51 +151,4 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
-theorem foldl_max
-    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
-    {l : List α} {a : α} :
-    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
-  cases l with
-  | nil => simp [Std.IdempotentOp.idempotent]
-  | cons b l =>
-    simp only [maximum?]
-    induction l generalizing a b with
-    | nil => simp
-    | cons c l ih => simp [ih, Std.Associative.assoc]
-
-theorem foldl_max_right {α β : Type _}
-    [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
-    {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
-  rw [← foldl_map, foldl_max]
-
-theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
-  induction l generalizing a with
-  | nil => simp
-  | cons c l ih =>
-    simp only [foldl_cons]
-    exact Nat.le_trans (Nat.le_max_left _ _) ih
-
-theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
-    a ≤ l.foldl (init := b) max :=
-  Nat.le_trans h (le_foldl_max)
-
-theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    a ≤ l.maximum?.getD k := by
-  cases l with
-  | nil => simp at h
-  | cons b l =>
-    simp [maximum?_cons]
-    simp at h
-    rcases h with (rfl | h)
-    · exact le_foldl_max
-    · induction l generalizing b with
-      | nil => simp_all
-      | cons c l ih =>
-        simp only [foldl_cons]
-        simp at h
-        rcases h with (rfl | h)
-        · exact le_foldl_max_of_le (Nat.le_max_right b a)
-        · exact ih _ h
-
 end List

src/Init/Data/List/Nat/Erase.lean

@@ -1,66 +0,0 @@
-/-
-Copyright (c) 2024 Kim Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Erase
-
-namespace List
-
-theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :
-    (l.eraseIdx i)[j]? = if h : j < i then l[j]? else l[j + 1]? := by
-  rw [eraseIdx_eq_take_drop_succ, getElem?_append]
-  split <;> rename_i h
-  · rw [getElem?_take]
-    split
-    · rfl
-    · simp_all
-      omega
-  · rw [getElem?_drop]
-    split <;> rename_i h'
-    · simp only [length_take, Nat.min_def, Nat.not_lt] at h
-      split at h
-      · omega
-      · simp_all [getElem?_eq_none]
-        omega
-    · simp only [length_take]
-      simp only [length_take, Nat.min_def, Nat.not_lt] at h
-      split at h
-      · congr 1
-        omega
-      · rw [getElem?_eq_none, getElem?_eq_none] <;> omega
-
-theorem getElem?_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < i) :
-    (l.eraseIdx i)[j]? = l[j]? := by
-  rw [getElem?_eraseIdx]
-  simp [h]
-
-theorem getElem?_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : i ≤ j) :
-    (l.eraseIdx i)[j]? = l[j + 1]? := by
-  rw [getElem?_eraseIdx]
-  simp only [dite_eq_ite, ite_eq_right_iff]
-  intro h'
-  omega
-
-theorem getElem_eraseIdx (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) :
-    (l.eraseIdx i)[j] = if h' : j < i then
-        l[j]'(by have := length_eraseIdx_le l i; omega)
-      else
-        l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
-  apply Option.some.inj
-  rw [← getElem?_eq_getElem, getElem?_eraseIdx]
-  split <;> simp
-
-theorem getElem_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : j < i) :
-    (l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega) := by
-  rw [getElem_eraseIdx]
-  simp only [dite_eq_left_iff, Nat.not_lt]
-  intro h'
-  omega
-
-theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : i ≤ j) :
-    (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
-  rw [getElem_eraseIdx, dif_neg]
-  omega

src/Init/Data/List/Nat/Find.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2024 Kim Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Data.List.Nat.Range
-import Init.Data.List.Find
-
-namespace List
-
-theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
-    (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
-  simp only [findIdx?_eq_findSome?_enum] at h
-  rw [findSome?_eq_some_iff] at h
-  simp only [Option.ite_none_right_eq_some, Option.some.injEq, ite_eq_right_iff, reduceCtorEq,
-    imp_false, Bool.not_eq_true, Prod.forall, exists_and_right, Prod.exists] at h
-  obtain ⟨h, h₁, b, ⟨es, h₂⟩, ⟨hb, rfl⟩, h₃⟩ := h
-  rw [enum_eq_enumFrom, enumFrom_eq_append_iff] at h₂
-  obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂
-  rw [eq_comm, enumFrom_eq_cons_iff] at h₂
-  obtain ⟨a, as, rfl, h₂, rfl⟩ := h₂
-  simp only [Nat.zero_add, Prod.mk.injEq] at h₂
-  obtain ⟨rfl, rfl⟩ := h₂
-  simp only [findIdx?_append]
-  match h : findIdx? q l₁' with
-  | some j =>
-    refine ⟨j, ?_, by simp⟩
-    rw [findIdx?_eq_some_iff_findIdx_eq] at h
-    omega
-  | none =>
-    refine ⟨l₁'.length, by simp, by simp_all⟩

src/Init/Data/List/Nat/Range.lean

@@ -358,6 +358,17 @@ theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
     map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
   induction l generalizing n <;> simp_all
 
+@[simp]
+theorem enumFrom_map_fst (n) :
+    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
+  | [] => rfl
+  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
+
+@[simp]
+theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
+  | _, [] => rfl
+  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
+
 theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l :=
   enumFrom_map_snd n l ▸ mem_map_of_mem _ h
 
@@ -380,6 +391,10 @@ theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enum
       x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
   ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩
 
+theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
+    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
+  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
+
 theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
     enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by
   induction l with
@@ -396,39 +411,22 @@ theorem enumFrom_append (xs ys : List α) (n : Nat) :
     rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
       Nat.add_assoc]
 
-theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
-    l.enumFrom n = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (n, a) ∧ l' = enumFrom (n + 1) as := by
-  rw [enumFrom_eq_zip_range', zip_eq_cons_iff]
-  constructor
-  · rintro ⟨l₁, l₂, h, rfl, rfl⟩
-    rw [range'_eq_cons_iff] at h
-    obtain ⟨rfl, -, rfl⟩ := h
-    exact ⟨x.2, l₂, by simp [enumFrom_eq_zip_range']⟩
-  · rintro ⟨a, as, rfl, rfl, rfl⟩
-    refine ⟨range' (n+1) as.length, as, ?_⟩
-    simp [enumFrom_eq_zip_range', range'_succ]
+theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
+  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
 
-theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
-    l.enumFrom n = l₁ ++ l₂ ↔
-      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length) := by
-  rw [enumFrom_eq_zip_range', zip_eq_append_iff]
-  constructor
-  · rintro ⟨w, x, y, z, h, h', rfl, rfl, rfl⟩
-    rw [range'_eq_append_iff] at h'
-    obtain ⟨k, -, rfl, rfl⟩ := h'
-    simp only [length_range'] at h
-    obtain rfl := h
-    refine ⟨y, z, rfl, ?_⟩
-    simp only [enumFrom_eq_zip_range', length_append, true_and]
-    congr
-    omega
-  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
-    simp only [enumFrom_eq_zip_range']
-    refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩
-    simp [Nat.add_comm]
+@[simp]
+theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
+    (l.enumFrom n).unzip = (range' n l.length, l) := by
+  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
 
 /-! ### enum -/
 
+theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
+
+theorem enum_cons' (x : α) (xs : List α) :
+    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
+  enumFrom_cons' _ _ _
+
 @[simp]
 theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
 

src/Init/Data/List/Range.lean

@@ -5,7 +5,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Pairwise
-import Init.Data.List.Zip
 
 /-!
 # Lemmas about `List.range` and `List.enum`
@@ -242,47 +241,4 @@ theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
     map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
   map_fst_add_enumFrom_eq_enumFrom l _ _
 
-theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
-    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
-  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
-
-@[simp]
-theorem enumFrom_map_fst (n) :
-    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
-  | [] => rfl
-  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
-
-@[simp]
-theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
-  | _, [] => rfl
-  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
-
-theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
-  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
-
-@[simp]
-theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
-    (l.enumFrom n).unzip = (range' n l.length, l) := by
-  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
-
-/-! ### enum -/
-
-theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
-
-theorem enum_cons' (x : α) (xs : List α) :
-    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
-  enumFrom_cons' _ _ _
-
-theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
-
-theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
-    enumFrom n l = (enum l).map (Prod.map (· + n) id) := by
-  induction l generalizing n with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
-      cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
-    intro a b _
-    exact (succ_add a n).symm
-
 end List

src/Init/Data/List/Zip.lean

@@ -16,6 +16,87 @@ open Nat
 
 /-! ## Zippers -/
 
+/-! ### zip -/
+
+theorem zip_map (f : α → γ) (g : β → δ) :
+    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
+  | [], l₂ => rfl
+  | l₁, [] => by simp only [map, zip_nil_right]
+  | a :: l₁, b :: l₂ => by
+    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
+
+theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
+    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
+
+theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
+    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
+
+@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
+    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
+  cases l₁ <;> cases l₂ <;> simp
+
+theorem zip_append :
+    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
+      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
+  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
+  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
+  | a :: l₁, r₁, b :: l₂, r₂, h => by
+    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
+
+theorem zip_map' (f : α → β) (g : α → γ) :
+    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
+  | [] => rfl
+  | a :: l => by simp only [map, zip_cons_cons, zip_map']
+
+theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
+  | _ :: l₁, _ :: l₂, h => by
+    cases h
+    case head => simp
+    case tail h =>
+    · have := of_mem_zip h
+      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
+
+@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
+
+theorem map_fst_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
+  | [], bs, _ => rfl
+  | _ :: as, _ :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.fst (zip as bs) = _ :: as
+    rw [map_fst_zip as bs h]
+  | a :: as, [], h => by simp at h
+
+theorem map_snd_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
+  | _, [], _ => by
+    rw [zip_nil_right]
+    rfl
+  | [], b :: bs, h => by simp at h
+  | a :: as, b :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.snd (zip as bs) = _ :: bs
+    rw [map_snd_zip as bs h]
+
+theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
+  rw [← zip_map']
+  congr
+  simp
+
+theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (f x, x)) = (l.map f).zip l := by
+  rw [← zip_map']
+  congr
+  simp
+
+/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
+@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
+    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
 /-! ### zipWith -/
 
 theorem zipWith_comm (f : α → β → γ) :
@@ -172,65 +253,6 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
       simp only [length_cons, Nat.succ.injEq] at h
       simp [ih _ h]
 
-theorem zipWith_eq_cons_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
-    zipWith f l₁ l₂ = g :: l ↔
-      ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂' := by
-  match l₁, l₂ with
-  | [], [] => simp
-  | [], b :: l₂ => simp
-  | a :: l₁, [] => simp
-  | a' :: l₁, b' :: l₂ =>
-    simp only [zip_cons_cons, cons.injEq, Prod.mk.injEq]
-    constructor
-    · rintro ⟨⟨rfl, rfl⟩, rfl⟩
-      refine ⟨a', l₁, b', l₂, by simp⟩
-    · rintro ⟨a, l₁, b, l₂, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl, rfl⟩
-      simp
-
-theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
-    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
-      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by
-  induction l₁ generalizing l₂ l₁' with
-  | nil =>
-    simp
-    constructor
-    · rintro ⟨rfl, rfl⟩
-      exact ⟨[], [], [], by simp⟩
-    · rintro ⟨_, _, _, -, ⟨rfl, rfl⟩, _, rfl, rfl, rfl⟩
-      simp
-  | cons x₁ l₁ ih₁ =>
-    cases l₂ with
-    | nil =>
-      constructor
-      · simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp]
-        rintro rfl  rfl
-        exact ⟨[], x₁ :: l₁, [], by simp⟩
-      · rintro ⟨w, x, y, z, h₁, _, h₃, rfl, rfl⟩
-        simp only [nil_eq, append_eq_nil] at h₃
-        obtain ⟨rfl, rfl⟩ := h₃
-        simp
-    | cons x₂ l₂ =>
-      simp only [zipWith_cons_cons]
-      rw [cons_eq_append_iff]
-      constructor
-      · rintro (⟨rfl, rfl⟩ | ⟨l₁'', rfl, h⟩)
-        · exact ⟨[], x₁ :: l₁, [], x₂ :: l₂, by simp⟩
-        · rw [ih₁] at h
-          obtain ⟨w, x, y, z, h, rfl, rfl, h', rfl⟩ := h
-          refine ⟨x₁ :: w, x, x₂ :: y, z, by simp [h, h']⟩
-      · rintro ⟨w, x, y, z, h₁, h₂, h₃, rfl, rfl⟩
-        rw [cons_eq_append_iff] at h₂
-        rw [cons_eq_append_iff] at h₃
-        obtain (⟨rfl, rfl⟩ | ⟨w', rfl, rfl⟩) := h₂
-        · simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
-          or_false]
-          obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
-          · simp
-          · simp_all
-        · obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
-          · simp_all
-          · simp_all [zipWith_append, Nat.succ_inj']
-
 /-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
 @[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
     zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
@@ -238,113 +260,6 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
   | zero => rfl
   | succ n ih => simp [replicate_succ, ih]
 
-/-! ### zip -/
-
-theorem zip_eq_zipWith : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂
-  | [], _ => rfl
-  | _, [] => rfl
-  | a :: l₁, b :: l₂ => by simp [zip_cons_cons, zip_eq_zipWith l₁ l₂]
-
-theorem zip_map (f : α → γ) (g : β → δ) :
-    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
-  | [], l₂ => rfl
-  | l₁, [] => by simp only [map, zip_nil_right]
-  | a :: l₁, b :: l₂ => by
-    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
-
-theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
-    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
-
-theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
-    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
-
-@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
-    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
-  cases l₁ <;> cases l₂ <;> simp
-
-theorem zip_append :
-    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
-      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
-  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
-  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
-  | a :: l₁, r₁, b :: l₂, r₂, h => by
-    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
-
-theorem zip_map' (f : α → β) (g : α → γ) :
-    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
-  | [] => rfl
-  | a :: l => by simp only [map, zip_cons_cons, zip_map']
-
-theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
-  | _ :: l₁, _ :: l₂, h => by
-    cases h
-    case head => simp
-    case tail h =>
-    · have := of_mem_zip h
-      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
-
-@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
-
-theorem map_fst_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
-  | [], bs, _ => rfl
-  | _ :: as, _ :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.fst (zip as bs) = _ :: as
-    rw [map_fst_zip as bs h]
-  | a :: as, [], h => by simp at h
-
-theorem map_snd_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
-  | _, [], _ => by
-    rw [zip_nil_right]
-    rfl
-  | [], b :: bs, h => by simp at h
-  | a :: as, b :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.snd (zip as bs) = _ :: bs
-    rw [map_snd_zip as bs h]
-
-theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
-    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
-  rw [← zip_map']
-  congr
-  simp
-
-theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
-    (l.map fun x => (f x, x)) = (l.map f).zip l := by
-  rw [← zip_map']
-  congr
-  simp
-
-@[simp] theorem zip_eq_nil_iff {l₁ : List α} {l₂ : List β} :
-    zip l₁ l₂ = [] ↔ l₁ = [] ∨ l₂ = [] := by
-  simp [zip_eq_zipWith]
-
-theorem zip_eq_cons_iff {l₁ : List α} {l₂ : List β} :
-    zip l₁ l₂ = (a, b) :: l ↔
-      ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zip l₁' l₂' := by
-  simp only [zip_eq_zipWith, zipWith_eq_cons_iff]
-  constructor
-  · rintro ⟨a, l₁, b, l₂, rfl, rfl, h, rfl, rfl⟩
-    simp only [Prod.mk.injEq] at h
-    obtain ⟨rfl, rfl⟩ := h
-    simp
-  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
-    refine ⟨a, l₁', b, l₂', by simp⟩
-
-theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
-    zip l₁ l₂ = l₁' ++ l₂' ↔
-      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by
-  simp [zip_eq_zipWith, zipWith_eq_append_iff]
-
-/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
-@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
-    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
-  induction n with
-  | zero => rfl
-  | succ n ih => simp [replicate_succ, ih]
-
 /-! ### zipWithAll -/
 
 theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :

src/Init/Data/Nat/Lemmas.lean

@@ -230,17 +230,6 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 @[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
   rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
 
-@[simp] theorem min_add_left {a b : Nat} : min a (b + a) = a := by
-  rw [Nat.min_def]
-  simp
-@[simp] theorem min_add_right {a b : Nat} : min a (a + b) = a := by
-  rw [Nat.min_def]
-  simp
-@[simp] theorem add_left_min {a b : Nat} : min (b + a) a = a := by
-  rw [Nat.min_comm, min_add_left]
-@[simp] theorem add_right_min {a b : Nat} : min (a + b) a = a := by
-  rw [Nat.min_comm, min_add_right]
-
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
   | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]
@@ -295,17 +284,6 @@ protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
 instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
-@[simp] theorem max_add_left {a b : Nat} : max a (b + a) = b + a := by
-  rw [Nat.max_def]
-  simp
-@[simp] theorem max_add_right {a b : Nat} : max a (a + b) = a + b := by
-  rw [Nat.max_def]
-  simp
-@[simp] theorem add_left_max {a b : Nat} : max (b + a) a = b + a := by
-  rw [Nat.max_comm, max_add_left]
-@[simp] theorem add_right_max {a b : Nat} : max (a + b) a = a + b := by
-  rw [Nat.max_comm, max_add_right]
-
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with
   | .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]

src/Init/Meta.lean

@@ -7,7 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Data.Array.GetLit
+import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
 
 namespace Lean

src/Init/Tactics.lean

@@ -773,9 +773,8 @@ macro_rules
 macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
-set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
+/-- Similar to `have`, but using `refine'` -/
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
-attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
 

src/Lean/Elab/InfoTree/Main.lean

@@ -183,7 +183,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
   f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
+  f!"FVarAlias {info.userName.eraseMacroScopes}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"

src/Lean/Linter/UnusedVariables.lean

@@ -447,10 +447,7 @@ def unusedVariables : Linter where
     let fvarAliases : Std.HashMap FVarId FVarId := s.fvarAliases.fold (init := {}) fun m id baseId =>
       m.insert id (followAliases s.fvarAliases baseId)
 
-    let getCanonVar (id : FVarId) : FVarId := fvarAliases.getD id id
-
     -- Collect all non-alias fvars corresponding to `fvarUses` by resolving aliases in the list.
-    -- Unlike `s.fvarUses`, `fvarUsesRef` is guaranteed to contain no aliases.
     let fvarUsesRef ← IO.mkRef <| fvarAliases.fold (init := s.fvarUses) fun fvarUses id baseId =>
       if fvarUses.contains id then fvarUses.insert baseId else fvarUses
 
@@ -464,7 +461,7 @@ def unusedVariables : Linter where
       let fvarUses ← fvarUsesRef.get
       -- If any of the `fvar`s corresponding to this declaration is (an alias of) a variable in
       -- `fvarUses`, then it is used
-      if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
+      if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
       -- If this is a global declaration then it is (potentially) used after the command
       if s.constDecls.contains range then continue
 
@@ -496,12 +493,10 @@ def unusedVariables : Linter where
       if !initializedMVars then
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
-        -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
-        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now
-        if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
+        if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
 
       -- If we made it this far then the variable is unused and not ignored
       unused := unused.push (declStx, userName)

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -55,8 +55,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.636 -> _uniq.312
-        • FVarAlias α: _uniq.635 -> _uniq.310
+        • FVarAlias a
+        • FVarAlias α
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -70,8 +70,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.667 -> _uniq.312
-        • FVarAlias n: _uniq.666 -> _uniq.310
+        • FVarAlias a
+        • FVarAlias n
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/linterUnusedVariables.lean

@@ -250,17 +250,6 @@ example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f
 example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
-inductive A where
-  | intro : Nat → A
-
-def A.out : A → Nat
-  | .intro n => n
-
-/-! `h` is used indirectly via an alias introduced by `match` that is used only via the mvar ctx -/
-theorem problematicAlias (n : A) (i : Nat) (h : i ≤ n.out) : i ≤ n.out :=
-  match n with
-  | .intro _ => by assumption
-
 /-!
 The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
 inaccessible annotation.