chore: run Batteries linter on Lean (#6364)

This PR makes fixes suggested by the Batteries environment linters,
particularly `simpNF`, and `unusedHavesSuffices`.

src/Init/Control/Lawful/Basic.lean

@@ -106,7 +106,7 @@ theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α 
 theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>= f = x >>= g := by
   simp [funext h]
 
-@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
+theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
   rw [bind_pure]
 
 theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by
@@ -133,7 +133,7 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y
   rw [← bind_pure_comp]
   simp only [bind_assoc, pure_bind]
 
-@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
+theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
   simp [map]
 
 /--

src/Init/Data/Array/Attach.lean

@@ -150,7 +150,6 @@ theorem attach_map_coe (l : Array α) (f : α → β) :
 theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
   attach_map_coe _ _
 
-@[simp]
 theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by
   cases l; simp
 
@@ -162,7 +161,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H :
     ((l.attachWith p H).map fun i => f i.val) = l.map f :=
   attachWith_map_coe _ _ _
 
-@[simp]
 theorem attachWith_map_subtype_val {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l := by
   cases l; simp
@@ -204,8 +202,8 @@ theorem pmap_ne_empty_iff {P : α → Prop} (f : (a : α) → P a → β) {xs :
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ #[] ↔ xs ≠ #[] := by
   cases xs; simp
 
-theorem pmap_eq_self {l : Array α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
-    (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
+theorem pmap_eq_self {l : Array α} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a}
+    {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
   cases l; simp [List.pmap_eq_self]
 
 @[simp]

src/Init/Data/Array/Basic.lean

@@ -79,7 +79,8 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 @[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 := rfl
+-- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
+theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 
@@ -208,7 +209,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩
 instance : Inhabited (Array α) where
   default := Array.empty
 
-@[simp] def isEmpty (a : Array α) : Bool :=
+def isEmpty (a : Array α) : Bool :=
   a.size = 0
 
 @[specialize]

src/Init/Data/Array/BasicAux.lean

@@ -32,10 +32,8 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
     have := Array.of_push_eq_push ih₂
     simp [this]
 
-@[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
-  apply propext; apply Iff.intro
-  · intro h; simpa [toArray] using h
-  · intro h; rw [h]
+theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
+  simp
 
 def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=
   go 0 ⟨mkEmpty as.size, rfl⟩ (by simp)

src/Init/Data/Array/Bootstrap.lean

@@ -93,11 +93,14 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
 @[simp] theorem appendList_eq_append
     (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
 
-@[simp] theorem appendList_toList (arr : Array α) (l : List α) :
+@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
     (arr ++ l).toList = arr.toList ++ l := by
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
+@[deprecated toList_appendList (since := "2024-12-11")]
+abbrev appendList_toList := @toList_appendList
+
 @[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
 theorem foldrM_eq_foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
@@ -149,7 +152,7 @@ abbrev pop_data := @pop_toList
 @[deprecated toList_append (since := "2024-09-09")]
 abbrev append_data := @toList_append
 
-@[deprecated appendList_toList (since := "2024-09-09")]
-abbrev appendList_data := @appendList_toList
+@[deprecated toList_appendList (since := "2024-09-09")]
+abbrev appendList_data := @toList_appendList
 
 end Array

src/Init/Data/Array/DecidableEq.lean

@@ -42,7 +42,7 @@ theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
   · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
-theorem isEqv_iff_rel (a b : Array α) (r) :
+theorem isEqv_iff_rel {a b : Array α} {r} :
     Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
   ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
     simp only [isEqv, ← h, ↓reduceDIte]

src/Init/Data/Array/Lemmas.lean

@@ -53,7 +53,7 @@ theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by
   cases l
   simpa using List.ne_nil_of_length_pos h
 
-@[simp] theorem size_eq_zero : l.size = 0 ↔ l = #[] :=
+theorem size_eq_zero : l.size = 0 ↔ l = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
 theorem size_pos_of_mem {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size := by
@@ -224,7 +224,7 @@ theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a
 
 /-! ### mem -/
 
-@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #[] := nofun
+theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
 
 @[simp] theorem mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by
   simp only [mem_def]
@@ -899,8 +899,8 @@ theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
 
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
-@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
-
+@[deprecated size_toArray (since := "2024-12-11")]
+theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
@@ -969,11 +969,6 @@ where
 @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
     arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
 
-@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
-    (arr ++ l).toList = arr.toList ++ l := by
-  cases arr
-  simp
-
 theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
     (F : Array β → α → Array β) (G : α → List β)
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -1014,7 +1009,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
+theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
     a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;>
   simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
@@ -1192,8 +1187,8 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j
 @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) :
     a.swapAt i v hi = (a[i], a.set i v) := rfl
 
-@[simp] theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) :
-    (a.swapAt i v hi).2.size = a.size := by simp [swapAt_def]
+theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) :
+    (a.swapAt i v hi).2.size = a.size := by simp
 
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
@@ -1687,13 +1682,9 @@ theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈
 @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
   simp only [size, toList_append, List.length_append]
 
-@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by
-  cases as
-  simp
+theorem empty_append (as : Array α) : #[] ++ as = as := by simp
 
-@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by
-  cases as
-  simp
+theorem append_empty (as : Array α) : as ++ #[] = as := by simp
 
 theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
     (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
@@ -2049,8 +2040,7 @@ namespace List
 Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 -/
 
-@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
-  simp
+theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by simp
 
 @[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
   apply ext'
@@ -2074,10 +2064,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
-    l.toArray.uset i a h = (l.set i.toNat a).toArray := by
-  apply ext'
-  simp
+theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
+    l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp
 
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
@@ -2113,7 +2101,8 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
     l.toArray.filterMap f = (l.filterMap f).toArray := by
   simp
 
-@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
+@[simp] theorem flatten_toArray (l : List (List α)) :
+    (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
 
@@ -2321,19 +2310,15 @@ end List
 
 namespace Array
 
-@[simp] theorem toList_fst_unzip (as : Array (α × β)) :
-    as.unzip.1.toList = as.toList.unzip.1 := by
-  cases as
-  simp
+theorem toList_fst_unzip (as : Array (α × β)) :
+    as.unzip.1.toList = as.toList.unzip.1 := by simp
 
-@[simp] theorem toList_snd_unzip (as : Array (α × β)) :
-    as.unzip.2.toList = as.toList.unzip.2 := by
-  cases as
-  simp
+theorem toList_snd_unzip (as : Array (α × β)) :
+    as.unzip.2.toList = as.toList.unzip.2 := by simp
 
 @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 
-@[simp] theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
+theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
     (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
   simp [flatMap]
   suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
@@ -2349,7 +2334,7 @@ namespace Array
   | nil => simp
   | cons a as ih =>
     apply ext'
-    simp [ih]
+    simp [ih, flatMap_toArray_cons]
 
 
 end Array