chore: follow simpNF linter's advice

src/Init/Control/Lawful/Instances.lean

@@ -188,7 +188,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
 
 @[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
 
-@[simp] theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
+theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
   simp [StateT.lift, StateT.run, bind, StateT.bind]
 
 @[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl

src/Init/Data/Array/Mem.lean

@@ -23,7 +23,7 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
 
-@[simp] theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 

src/Init/Data/BitVec/Lemmas.lean

@@ -110,8 +110,8 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
 theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
 
 @[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
-@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
-@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
+theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp
+theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp
 @[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
@@ -329,7 +329,7 @@ theorem zeroExtend'_eq {x : BitVec w} (h : w ≤ v) : x.zeroExtend' h = x.zeroEx
   apply eq_of_toNat_eq
   simp [toNat_zeroExtend]
 
-@[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
+theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
 
 @[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = truncate m x := by
   apply eq_of_toNat_eq
@@ -383,7 +383,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
   all_goals (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
     <;> omega
 
-@[simp] theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
   getLsb_zeroExtend m x i
 
@@ -608,7 +608,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp_all [lt_of_getLsb]
 
-@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x ^^^ cast h y = cast h (x ^^^ y) := by
   ext
   simp_all [lt_of_getLsb]
 

src/Init/Data/Bool.lean

@@ -52,8 +52,8 @@ theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
 @[simp] theorem decide_eq_true  {b : Bool} [Decidable (b = true)]  : decide (b = true)  =  b := by cases b <;> simp
 @[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp
-@[simp] theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
-@[simp] theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
+theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
+theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
 
 /-! ### and -/
 
@@ -163,7 +163,7 @@ Consider the term: `¬((b && c) = true)`:
 -/
 @[simp] theorem and_eq_false_imp : ∀ (x y : Bool), (x && y) = false ↔ (x = true → y = false) := by decide
 
-@[simp] theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
+theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by simp
 
 @[simp] theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
 
@@ -187,11 +187,9 @@ in false_eq and true_eq.
 
 @[simp] theorem true_beq  : ∀b, (true  == b) =  b := by decide
 @[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
-@[simp] theorem beq_true  : ∀b, (b == true)  =  b := by decide
 instance : Std.LawfulIdentity (· == ·) true where
   left_id := true_beq
   right_id := beq_true
-@[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
 
 @[simp] theorem true_bne  : ∀(b : Bool), (true  != b) = !b := by decide
 @[simp] theorem false_bne : ∀(b : Bool), (false != b) =  b := by decide
@@ -353,7 +351,7 @@ theorem and_or_inj_left_iff :
 /-! ## toNat -/
 
 /-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
-def toNat (b:Bool) : Nat := cond b 1 0
+def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp] theorem toNat_false : false.toNat = 0 := rfl
 

src/Init/Data/List/Basic.lean

@@ -88,7 +88,7 @@ namespace List
 
 /-! ### concat -/
 
-@[simp] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
+@[simp high] 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]
@@ -817,6 +817,8 @@ def dropLast {α} : List α → List α
 @[simp] theorem dropLast_cons₂ :
     (x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
 
+-- Later this can be proved by `simp` via `[List.length_dropLast, List.length_cons, Nat.add_sub_cancel]`,
+-- but we need this while bootstrapping `Array`.
 @[simp] theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length := by
   match as with
   | []       => rfl

src/Init/Data/List/Lemmas.lean

@@ -168,11 +168,20 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
 
 @[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
 
+@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
+  simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
+
+theorem getElem?_eq_some {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]
+
+@[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
+  simp only [← get?_eq_getElem?, get?_eq_none]
+
+theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
+
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
-@[simp] theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by
-  simp only [← get?_eq_getElem?]
-  rfl
+theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 
 @[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
   simp only [← get?_eq_getElem?]
@@ -183,17 +192,6 @@ theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
   | _ :: l, _+1, h => by
     rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h]
 
-@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
-  simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
-
-theorem getElem?_eq_some {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]
-
-@[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
-  simp only [← get?_eq_getElem?, get?_eq_none]
-
-theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
-
 @[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 @[simp] theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
@@ -820,9 +818,8 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
 @[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
   cases l <;> rfl
 
-@[simp] theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
-    tailD (map f l) (map f l') = map f (tailD l l') := by
-  cases l <;> rfl
+theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
+    tailD (map f l) (map f l') = map f (tailD l l') := by simp
 
 @[simp] theorem getLast_map (f : α → β) (l : List α) (h) :
     getLast (map f l) h = f (getLast l (by simpa using h)) := by
@@ -1538,8 +1535,7 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 
 /-! ### elem / contains -/
 
-@[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
-  simp [elem_cons]
+theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
 @[simp] theorem contains_cons [BEq α] :
     (a :: as : List α).contains x = (x == a || as.contains x) := by
@@ -1944,15 +1940,14 @@ end replace
 section insert
 variable [BEq α] [LawfulBEq α]
 
-@[simp] theorem insert_nil (a : α) : [].insert a = [a] := by
-  simp [List.insert]
-
 @[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
   simp [List.insert, h]
 
 @[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by
   simp [List.insert, h]
 
+theorem insert_nil (a : α) : [].insert a = [a] := by simp
+
 @[simp] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
   if h : b ∈ l then
     rw [insert_of_mem h]

src/Init/Data/Nat/Basic.lean

@@ -124,13 +124,8 @@ instance : LawfulBEq Nat where
   eq_of_beq h := Nat.eq_of_beq_eq_true h
   rfl := by simp [BEq.beq]
 
-@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
-@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
-  propext <| Iff.intro
-    (fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
-    (fun h =>
-      have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
-      by simp [this])
+theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp
+theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp
 
 /-! # Nat.add theorems -/
 
@@ -355,7 +350,7 @@ protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_po
 
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
-@[simp] theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
+theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
 @[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
 
@@ -705,8 +700,7 @@ protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
 protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
   fun h => Nat.noConfusion h
 
-@[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 :=
-  fun h => Nat.noConfusion h
+theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
 /-! # mul + order -/
 
@@ -814,8 +808,11 @@ theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
 
 /-! # pred theorems -/
 
-@[simp] protected theorem pred_zero : pred 0 = 0 := rfl
-@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
+protected theorem pred_zero : pred 0 = 0 := rfl
+protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
+
+@[simp] protected theorem zero_sub_one : 0 - 1 = 0 := rfl
+@[simp] protected theorem add_one_sub_one (n : Nat) : n + 1 - 1 = n := rfl
 
 theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
   induction a with

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -86,7 +86,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
 @[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
   cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
 
-@[simp] theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 

src/Init/Data/Nat/Lemmas.lean

@@ -115,8 +115,6 @@ protected theorem add_sub_cancel_right (n m : Nat) : (n + m) - m = n := Nat.add_
 
 theorem succ_sub_one (n) : succ n - 1 = n := rfl
 
-protected theorem add_one_sub_one (n : Nat) : (n + 1) - 1 = n := rfl
-
 protected theorem one_add_sub_one (n : Nat) : (1 + n) - 1 = n := Nat.add_sub_cancel_left 1 _
 
 protected theorem sub_sub_self {n m : Nat} (h : m ≤ n) : n - (n - m) = m :=

src/Init/PropLemmas.lean

@@ -368,9 +368,6 @@ else isTrue fun h2 => absurd h2 h
 
 theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp
 
-@[simp] theorem decide_eq_false_iff_not (p : Prop) {_ : Decidable p} : (decide p = false) ↔ ¬p :=
-  ⟨of_decide_eq_false, decide_eq_false⟩
-
 @[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
     decide p = decide q ↔ (p ↔ q) :=
   ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩

src/Init/SimpLemmas.lean

@@ -228,36 +228,33 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 @[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
 @[simp] theorem Bool.not_true  : (!true) = false := by decide
 @[simp] theorem Bool.not_false : (!false) = true := by decide
-@[simp] theorem Bool.not_beq_true  (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
-@[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
+@[simp] theorem beq_true  (b : Bool) : (b == true)  =  b := by cases b <;> rfl
+@[simp] theorem beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
 @[simp] theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
 @[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
 
-@[simp] theorem Bool.beq_to_eq (a b : Bool) :
-  (a == b) = (a = b) := by cases a <;> cases b <;> decide
-@[simp] theorem Bool.not_beq_to_not_eq (a b : Bool) :
-  (!(a == b)) = ¬(a = b) := by cases a <;> cases b <;> decide
-
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
 
 @[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
   propext <| Iff.intro of_decide_eq_true decide_eq_true
+@[simp] theorem decide_eq_false_iff_not {_ : Decidable p} : (decide p = false) ↔ ¬p :=
+  ⟨of_decide_eq_false, decide_eq_false⟩
+
 @[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
-  cases h <;> (rename_i hp; simp [decide, hp])
+@[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
 
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
 
 @[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl
-@[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
+theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp
 
 @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
-@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
+theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp
 
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True  : decide True  = true := rfl
@@ -283,7 +280,10 @@ These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`.
   rw [bne, ← beq_iff_eq a b]
   cases a == b <;> decide
 
-/-# Nat -/
+theorem Bool.beq_to_eq (a b : Bool) : (a == b) = (a = b) := by simp
+theorem Bool.not_beq_to_not_eq (a b : Bool) : (!(a == b)) = ¬(a = b) := by simp
+
+/- # Nat -/
 
 @[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
   propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩

tests/lean/run/exfalsoBug.lean

@@ -78,8 +78,6 @@ theorem f_eq (n : Nat) :
       cases n <;> simp [f']
       next => contradiction
       next n _ =>
-       have : Nat.succ n - 1 = n := rfl
-       rw [this]
        split <;> try simp
        next r hrn h₁ =>
          split <;> simp