chore: running the simpNF linter over Lean (#5133)

This should resolve nearly all of the simpNF lints. This is a follow-up
to #4620.

src/Init/Data/BitVec/Lemmas.lean

@@ -413,11 +413,9 @@ theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := b
     (x.truncate l).truncate k = x.truncate k :=
   zeroExtend_zeroExtend_of_le x h
 
-/--Truncating by the bitwidth has no effect. -/
-@[simp]
-theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := by
-  ext i
-  simp [getLsb_zeroExtend]
+/-- Truncating by the bitwidth has no effect. -/
+-- This doesn't need to be a `@[simp]` lemma, as `zeroExtend_eq` applies.
+theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := zeroExtend_eq _
 
 @[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
   apply eq_of_getLsb_eq
@@ -776,7 +774,6 @@ theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
 @[simp]
 theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := by rfl
 
-@[simp]
 theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x := by simp
 
 theorem shiftLeft_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃} :

src/Init/Data/List/Basic.lean

@@ -96,7 +96,7 @@ namespace List
 
 /-! ### concat -/
 
-@[simp high] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
+theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
   induction as with
   | nil => rfl
   | cons _ xs ih => simp [concat, ih]
@@ -278,8 +278,9 @@ def getLastD : (as : List α) → (fallback : α) → α
   | [],   a₀ => a₀
   | a::as, _ => getLast (a::as) (fun h => List.noConfusion h)
 
-@[simp] theorem getLastD_nil (a) : @getLastD α [] a = a := rfl
-@[simp] theorem getLastD_cons (a b l) : @getLastD α (b::l) a = getLastD l b := by cases l <;> rfl
+-- These aren't `simp` lemmas since we always simplify `getLastD` in terms of `getLast?`.
+theorem getLastD_nil (a) : @getLastD α [] a = a := rfl
+theorem getLastD_cons (a b l) : @getLastD α (b::l) a = getLastD l b := by cases l <;> rfl
 
 /-! ## Head and tail -/
 

src/Init/Data/List/BasicAux.lean

@@ -222,7 +222,7 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as
   next => apply append_cancel_right
   next => intro h; simp [h]
 
-@[simp] theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
   match as, i with
   | a::as, ⟨0, _⟩  => simp_arith [get]
   | a::as, ⟨i+1, h⟩ =>

src/Init/Data/List/Find.lean

@@ -298,7 +298,8 @@ theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
-@[simp] theorem find?_replicate_eq_none (n : Nat) (a : α) (p : α → Bool) :
+-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
+theorem find?_replicate_eq_none (n : Nat) (a : α) (p : α → Bool) :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 

src/Init/Data/List/Lemmas.lean

@@ -379,19 +379,15 @@ theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a =
 theorem forall_mem_ne' {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l :=
   ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
 
-@[simp]
 theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
   induction l <;> simp_all
 
-@[simp]
 theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
   induction l <;> simp_all [eq_comm (a := a)]
 
-@[simp]
 theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
   induction l <;> simp_all
 
-@[simp]
 theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
   induction l <;> simp_all [eq_comm (a := a)]
 
@@ -515,7 +511,7 @@ theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 :=
 @[simp] theorem isEmpty_eq_true {l : List α} : l.isEmpty ↔ l = [] := by
   cases l <;> simp
 
-@[simp] theorem isEmpty_eq_false {l : List α} : ¬ l.isEmpty ↔ l ≠ [] := by
+@[simp] theorem isEmpty_eq_false {l : List α} : l.isEmpty = false ↔ l ≠ [] := by
   cases l <;> simp
 
 /-! ### any / all -/
@@ -555,7 +551,7 @@ theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length)
   simp_all [getElem?_eq_some]
 
 @[simp]
-theorem getElem?_set_eq' {l : List α} {i : Nat} {a : α} : (set l i a)[i]? = (fun _ => a) <$> l[i]? := by
+theorem getElem?_set_eq' {l : List α} {i : Nat} {a : α} : (set l i a)[i]? = Function.const _ a <$> l[i]? := by
   by_cases h : i < l.length
   · simp [getElem?_set_eq h, getElem?_eq_getElem h]
   · simp only [Nat.not_lt] at h
@@ -612,7 +608,7 @@ theorem getElem?_set {l : List α} {i j : Nat} {a : α} :
 theorem getElem?_set' {l : List α} {i j : Nat} {a : α} :
     (set l i a)[j]? = if i = j then (fun _ => a) <$> l[j]? else l[j]? := by
   by_cases i = j
-  · simp only [getElem?_set_eq', Option.map_eq_map, ↓reduceIte, *]
+  · simp only [getElem?_set_eq', Option.map_eq_map, ↓reduceIte, *]; rfl
   · simp only [ne_eq, not_false_eq_true, getElem?_set_ne, ↓reduceIte, *]
 
 theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} :
@@ -892,7 +888,7 @@ theorem getLast?_eq_get? (l : List α) : getLast? l = l.get? (l.length - 1) := b
 @[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
   simp [getLast?_eq_getElem?, Nat.succ_sub_succ]
 
-@[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
+theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl
 
 /-! ## Head and tail -/
@@ -1504,9 +1500,9 @@ theorem getElem?_append {l₁ l₂ : List α} {n : Nat} :
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)
 
-@[simp] theorem head_append_of_ne_nil {l : List α} (w : l ≠ []) :
-    head (l ++ l') (by simp_all) = head l w := by
-  match l, w with
+@[simp] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
+    head (l ++ l') w₁ = head l w₂ := by
+  match l, w₂ with
   | a :: l, _ => rfl
 
 theorem head_append {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) :
@@ -2135,18 +2131,19 @@ theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (rep
   | nil => rfl
   | cons a as ih => simp [ih]
 
-@[simp] theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs
+theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs
   | [], _ => ⟨.inr, fun | .inr h => h⟩
   | a :: _, _ => by rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons]
 
-@[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by simp [reverse]
+@[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by
+  simp [reverse, mem_reverseAux]
 
 @[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = [] := by
   match xs with
   | [] => simp
   | x :: xs => simp
 
-@[simp] theorem reverse_ne_nil_iff {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ [] :=
+theorem reverse_ne_nil_iff {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ [] :=
   not_congr reverse_eq_nil_iff
 
 theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
@@ -2290,8 +2287,8 @@ theorem head_eq_getLast_reverse {l : List α} (h : l ≠ []) :
     l.head h = l.reverse.getLast (by simp_all) := by
   rw [← getLast_reverse]
 
-@[simp] theorem getLast_append_of_ne_nil {l : List α} (h : l' ≠ []) :
-    (l ++ l').getLast (append_ne_nil_of_right_ne_nil l h) = l'.getLast (by simp_all) := by
+@[simp] theorem getLast_append_of_ne_nil {l : List α} {h₁} (h₂ : l' ≠ []) :
+    (l ++ l').getLast h₁ = l'.getLast h₂ := by
   simp only [getLast_eq_head_reverse, reverse_append]
   rw [head_append_of_ne_nil]
 
@@ -2463,8 +2460,8 @@ theorem dropLast_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).dropLast = if l₂.isEmpty then l₁.dropLast else l₁ ++ l₂.dropLast := by
   split <;> simp_all
 
-@[simp] theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b::l₂) := by
-  simp only [ne_eq, not_false_eq_true, dropLast_append_of_ne_nil]
+theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b::l₂) := by
+  simp
 
 @[simp 1100] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp
 

src/Init/Data/List/Perm.lean

@@ -123,10 +123,8 @@ theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm
 
 @[simp] theorem nil_perm {l₁ : List α} : [] ~ l₁ ↔ l₁ = [] := perm_comm.trans perm_nil
 
-@[simp]
 theorem not_perm_nil_cons (x : α) (l : List α) : ¬[] ~ x :: l := (nomatch ·.symm.eq_nil)
 
-@[simp]
 theorem not_perm_cons_nil {l : List α} {a : α} : ¬(Perm (a::l) []) :=
   fun h => by simpa using h.length_eq
 

src/Init/Data/List/TakeDrop.lean

@@ -95,9 +95,7 @@ theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m
 theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
   simp [getElem?_take_of_lt, h]
 
-@[simp]
-theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? :=
-  getElem?_take_of_lt (Nat.lt_succ_self n)
+theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
 
 @[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
   | m, [] => by simp

src/Init/Data/Nat/Basic.lean

@@ -158,7 +158,7 @@ theorem add_one (n : Nat) : n + 1 = succ n :=
   rfl
 
 @[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
-@[simp] theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := nofun
+theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := by simp
 
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
   | n, 0   => Eq.symm (Nat.zero_add n)

src/Init/SimpLemmas.lean

@@ -244,7 +244,7 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 
 @[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
   cases g <;> (rename_i gp; simp [gp]; rfl)
-@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp
+theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp
 
 @[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
 

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -26,6 +26,8 @@ open List (Perm)
 
 namespace Std.DHashMap.Internal.List
 
+attribute [-simp] List.isEmpty_eq_false
+
 @[elab_as_elim]
 theorem assoc_induction {motive : List ((a : α) × β a) → Prop} (nil : motive [])
     (cons : (k : α) → (v : β k) → (tail : List ((a : α) × β a)) →