chore: review Array operations argument order

src/Init/Data/Array/Basic.lean

@@ -247,7 +247,7 @@ def get? (a : Array α) (i : Nat) : Option α :=
   if h : i < a.size then some a[i] else none
 
 def back? (a : Array α) : Option α :=
-  a[a.size - 1]?
+  a.get? (a.size - 1)
 
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a[i]
@@ -442,8 +442,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
-@[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
-
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]

src/Init/Data/Array/Lemmas.lean

@@ -76,8 +76,6 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
-theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
-
 end Array
 
 namespace List
@@ -113,9 +111,6 @@ We prefer to pull `List.toArray` outwards.
 @[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
   simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
 
-@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
-  simp [back?, List.getLast?_eq_getElem?]
-
 @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
     (h : i ≤ l.length) (b : β) :
     Array.forIn'.loop l.toArray f i h b =
@@ -586,8 +581,6 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
 
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
-theorem mkArray_eq_toArray_replicate (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray := rfl
-
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
     (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 

src/Init/Data/List/Find.lean

@@ -10,8 +10,7 @@ import Init.Data.List.Sublist
 import Init.Data.List.Range
 
 /-!
-Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `List.indexOf`,
-and `List.lookup`.
+# Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, and `List.indexOf`.
 -/
 
 namespace List
@@ -96,22 +95,22 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
     · simp only [Option.guard_eq_none] at h
       simp [ih, h]
 
-@[simp] theorem head?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
+@[simp] theorem filterMap_head? (f : α → Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [filterMap_cons, findSome?_cons]
     split <;> simp [*]
 
-@[simp] theorem head_filterMap (f : α → Option β) (l : List α) (h) :
-    (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
+@[simp] theorem filterMap_head (f : α → Option β) (l : List α) (h) :
+    (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none])  := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem getLast?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
+@[simp] theorem filterMap_getLast? (f : α → Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
   rw [getLast?_eq_head?_reverse]
   simp [← filterMap_reverse]
 
-@[simp] theorem getLast_filterMap (f : α → Option β) (l : List α) (h) :
+@[simp] theorem filterMap_getLast (f : α → Option β) (l : List α) (h) :
     (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast_eq_some]
 
@@ -292,18 +291,18 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
     · simp only [find?_cons]
       split <;> simp_all
 
-@[simp] theorem head?_filter (p : α → Bool) (l : List α) : (l.filter p).head? = l.find? p := by
-  rw [← filterMap_eq_filter, head?_filterMap, findSome?_guard]
+@[simp] theorem filter_head? (p : α → Bool) (l : List α) : (l.filter p).head? = l.find? p := by
+  rw [← filterMap_eq_filter, filterMap_head?, findSome?_guard]
 
-@[simp] theorem head_filter (p : α → Bool) (l : List α) (h) :
+@[simp] theorem filter_head (p : α → Bool) (l : List α) (h) :
     (l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem getLast?_filter (p : α → Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
+@[simp] theorem filter_getLast? (p : α → Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
   rw [getLast?_eq_head?_reverse]
   simp [← filter_reverse]
 
-@[simp] theorem getLast_filter (p : α → Bool) (l : List α) (h) :
+@[simp] theorem filter_getLast (p : α → Bool) (l : List α) (h) :
     (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast_eq_some]
 

src/Init/Data/List/Lemmas.lean

@@ -1045,7 +1045,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
 
 @[simp] theorem getLast_singleton (a h) : @getLast α [a] h = a := rfl
 
-theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
+theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
   simp [getLast!, getLast_eq_getLastD]
 
 @[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
@@ -1109,12 +1109,7 @@ theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
 
 /-! ### getLast! -/
 
-theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
-
-@[simp] theorem getLast!_eq_getLast?_getD [Inhabited α] {l : List α} : getLast! l = (getLast? l).getD default := by
-  cases l with
-  | nil => simp [getLast!_nil]
-  | cons _ _ => simp [getLast!, getLast?_eq_getLast]
+@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
 
 theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
   | _ :: _, rfl => rfl

src/Init/Data/Option/Basic.lean

@@ -25,9 +25,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM
   | some _ => true
   | none   => false
 
-@[simp] theorem isSome_none : @isSome α none = false := rfl
-@[simp] theorem isSome_some : isSome (some a) = true := rfl
-
 @[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
 
 /-- Returns `true` on `none` and `false` on `some x`. -/
@@ -35,9 +32,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM
   | some _ => false
   | none   => true
 
-@[simp] theorem isNone_none : @isNone α none = true := rfl
-@[simp] theorem isNone_some : isNone (some a) = false := rfl
-
 /--
 `x?.isEqSome y` is equivalent to `x? == some y`, but avoids an allocation.
 -/
@@ -140,10 +134,6 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
 @[inline] def get {α : Type u} : (o : Option α) → isSome o → α
   | some x, _ => x
 
-@[simp] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
-| some _, _ => rfl
-@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
-
 /-- `guard p a` returns `some a` if `p a` holds, otherwise `none`. -/
 @[inline] def guard (p : α → Prop) [DecidablePred p] (a : α) : Option α :=
   if p a then some a else none

src/Init/Data/Option/Lemmas.lean

@@ -36,6 +36,11 @@ theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a
 
 theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun
 
+@[simp] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
+| some _, _ => rfl
+
+@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
+
 theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x := by
   cases x; {contradiction}; rw [getD_some]
 
@@ -68,11 +73,19 @@ theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a
 theorem eq_none_iff_forall_not_mem : o = none ↔ ∀ a, a ∉ o :=
   ⟨fun e a h => by rw [e] at h; (cases h), fun h => ext <| by simp; exact h⟩
 
+@[simp] theorem isSome_none : @isSome α none = false := rfl
+
+@[simp] theorem isSome_some : isSome (some a) = true := rfl
+
 theorem isSome_iff_exists : isSome x ↔ ∃ a, x = some a := by cases x <;> simp [isSome]
 
 theorem isSome_eq_isSome : (isSome x = isSome y) ↔ (x = none ↔ y = none) := by
   cases x <;> cases y <;> simp
 
+@[simp] theorem isNone_none : @isNone α none = true := rfl
+
+@[simp] theorem isNone_some : isNone (some a) = false := rfl
+
 @[simp] theorem not_isSome : isSome a = false ↔ a.isNone = true := by
   cases a <;> simp
 

src/Init/GetElem.lean

@@ -166,12 +166,6 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
   have : Decidable (dom c i) := .isFalse h
   simp [getElem!_def, getElem?_def, h]
 
-@[simp] theorem get_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) [Decidable (dom c i)] (h) :
-    c[i]?.get h = c[i]'(by simp only [getElem?_def] at h; split at h <;> simp_all) := by
-  simp only [getElem?_def] at h ⊢
-  split <;> simp_all
-
 namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where

src/Init/Prelude.lean

@@ -2829,6 +2829,17 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabi
 instance [Monad m] : [Nonempty α] → Nonempty (m α)
   | ⟨x⟩ => ⟨pure x⟩
 
+/-- A fusion of Haskell's `sequence` and `map`. Used in syntax quotations. -/
+def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m β) : m (Array β) :=
+  let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=
+    dite (LT.lt j as.size)
+      (fun hlt =>
+        match i with
+        | 0           => pure bs
+        | Nat.succ i' => Bind.bind (f (as.get j hlt)) fun b => loop i' (hAdd j 1) (bs.push b))
+      (fun _ => pure bs)
+  loop as.size 0 (Array.mkEmpty as.size)
+
 /--
 A function for lifting a computation from an inner `Monad` to an outer `Monad`.
 Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -87,7 +87,7 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
     xs.mapM (·.fvarId!.getUserName)
 
 def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
-  let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
+  let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do

src/Lean/Elab/Quotation.lean

@@ -434,7 +434,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else mkNullNode contents
           -- We use `no_error_if_unused%` in auxiliary `match`-syntax to avoid spurious error messages,
           -- the outer `match` is checking for unused alternatives
-          `(match ($(discrs).mapM fun
+          `(match ($(discrs).sequenceMap fun
                 | `($contents) => no_error_if_unused% some $tuple
                 | _            => no_error_if_unused% none) with
               | some $resId => $yes