fix

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]
@@ -912,8 +912,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
@@ -982,11 +982,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) :
@@ -1027,7 +1022,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?]
@@ -1205,8 +1200,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) :
@@ -1700,13 +1695,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
@@ -2062,8 +2053,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'
@@ -2087,10 +2077,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
@@ -2126,7 +2114,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]
 
@@ -2334,19 +2323,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 =
@@ -2362,7 +2347,7 @@ namespace Array
   | nil => simp
   | cons a as ih =>
     apply ext'
-    simp [ih]
+    simp [ih, flatMap_toArray_cons]
 
 
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -332,11 +332,11 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
-@[simp] theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
-  simp [getElem_eq_testBit_toNat]
+theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
+  simp
 
-@[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
-  simp [getElem_eq_testBit_toNat, h]
+theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
+  simp
 
 theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
   simp
@@ -362,12 +362,7 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-@[simp]
-theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
-  rcases b with rfl | rfl
-  · simp [ofBool]
-  · simp only [ofBool]
-    by_cases hi : i = 0 <;> simp [hi] <;> omega
+theorem getElem_ofBool {b : Bool} : (ofBool b)[0] = b := by simp
 
 @[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
   cases b <;> simp [getMsbD]
@@ -538,7 +533,7 @@ theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
 A bitvector, when interpreted as an integer, is less than zero iff
 its most significant bit is true.
 -/
-theorem slt_zero_iff_msb_cond (x : BitVec w) : x.slt 0#w ↔ x.msb = true := by
+theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
   have := toInt_eq_msb_cond x
   constructor
   · intros h
@@ -1120,12 +1115,8 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     rw [h]
     simp
 
-@[simp] theorem getMsb_not {x : BitVec w} :
-    (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by
-  simp only [getMsbD]
-  by_cases h : i < w
-  · simp [h]; omega
-  · simp [h];
+theorem getMsb_not {x : BitVec w} :
+    (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by simp
 
 @[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
   simp [BitVec.msb]
@@ -1243,7 +1234,6 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 
 @[simp] theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
     getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i := by
-  have : n ≤ i + n := by omega
   simp_all [shiftLeftZeroExtend_eq]
 
 @[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
@@ -1291,10 +1281,9 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
     (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
   simp [shiftLeft_eq', getLsbD_shiftLeft]
 
-@[simp]
 theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) :
     (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
-  simp [shiftLeft_eq', getLsbD_shiftLeft]
+  simp
 
 /-! ### ushiftRight -/
 
@@ -1597,39 +1586,25 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
 @[simp]
 theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl
 
-@[simp]
-theorem getLsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
+-- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form.
+theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} :
     getLsbD (x.sshiftRight' y) i =
       (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
   simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
 
-@[simp]
+-- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form.
 theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) :
     (x.sshiftRight' y)[i] =
       (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
   simp only [← getLsbD_eq_getElem, BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
 
-@[simp]
 theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
-    (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
-  simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight]
-  by_cases h : i < w
-  · simp only [h, decide_true, Bool.true_and]
-    by_cases h₁ : w ≤ w - 1 - i
-    · simp [h₁]
-      omega
-    · simp only [h₁, decide_false, Bool.not_false, Bool.true_and]
-      by_cases h₂ : i < y.toNat
-      · simp only [h₂, ↓reduceIte, ite_eq_right_iff]
-        omega
-      · simp only [show i - y.toNat < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and]
-        by_cases h₄ : y.toNat + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)
-  · simp [h]
+    (x.sshiftRight y.toNat).getMsbD i =
+      (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
+  simp
 
-@[simp]
 theorem msb_sshiftRight' {x y: BitVec w} :
-    (x.sshiftRight' y).msb = x.msb := by
-  simp [BitVec.sshiftRight', BitVec.msb_sshiftRight]
+    (x.sshiftRight' y).msb = x.msb := by simp
 
 /-! ### signExtend -/
 
@@ -1883,7 +1858,6 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
   · simp_all
   · simp_all only [Bool.iff_and_self, decide_eq_true_eq]
     intro h
-    have := BitVec.lt_of_getLsbD h
     omega
 
 @[simp] theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by
@@ -2091,8 +2065,9 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
 @[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
   simp [getLsbD_concat]
 
-@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i < w) :
+@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i + 1 < w + 1) :
     (concat x b)[i + 1] = x[i] := by
+  simp only [Nat.add_lt_add_iff_right] at h
   simp [getElem_concat, h, getLsbD_eq_getElem]
 
 @[simp]
@@ -2195,7 +2170,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
     (hk : k < w) (hx : x.toNat < 2 ^ k) :
     (x.shiftConcat b).toNat < 2 ^ (k + 1) := by
   rw [toNat_shiftConcat_eq_of_lt hk hx]
-  have : 2 ^ (k + 1) ≤ 2 ^ w := Nat.pow_le_pow_of_le_right (by decide) (by assumption)
   have := Bool.toNat_lt b
   omega
 
@@ -2704,7 +2678,7 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
 
 @[simp]
 theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by
-  rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond x, hx, ← negOne_eq_allOnes]
+  rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, ← negOne_eq_allOnes]
 
 /-! ### srem -/
 
@@ -3024,10 +2998,10 @@ theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega]
 
 /-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/
-@[simp]
-theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w):
+-- This should not be a simp lemma as `getMsbD_rotateRight` will apply first.
+theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w) :
     (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
-    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
+    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))) := by
   rcases w with rfl | w
   · simp
   · rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]
@@ -3590,9 +3564,7 @@ Note, however, that for large numerals the decision procedure may be very slow.
 instance instDecidableExistsBitVec :
     ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∃ v, P v)
   | 0, _, _ => inferInstance
-  | n + 1, _, _ =>
-    have := instDecidableExistsBitVec n
-    inferInstance
+  | _ + 1, _, _ => inferInstance
 
 /-! ### Deprecations -/
 

src/Init/Data/Bool.lean

@@ -225,7 +225,7 @@ theorem bne_not_self : ∀ (x : Bool), (x   != !x) = true := by decide
 Added for equivalence with `Bool.not_beq_self` and needed for confluence
 due to `beq_iff_eq`.
 -/
-@[simp] theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by decide
+theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by simp
 @[simp] theorem eq_not_self : ∀(b : Bool), (b = (!b)) ↔ False := by decide
 
 @[simp] theorem beq_self_left  : ∀(a b : Bool), (a == (a == b)) = b := by decide
@@ -420,7 +420,7 @@ def toInt (b : Bool) : Int := cond b 1 0
 
 @[simp] theorem ite_eq_true_else_eq_false {q : Prop} :
     (if b = true then q else b = false) ↔ (b = true → q) := by
-  cases b <;> simp
+  cases b <;> simp [not_eq_self]
 
 /-
 `not_ite_eq_true_eq_true` and related theorems below are added for

src/Init/Data/Fin/Lemmas.lean

@@ -545,10 +545,8 @@ theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
     natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) :=
   Fin.ext <| (Nat.add_assoc ..).symm
 
-@[simp]
 theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
-    (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) :=
-  Fin.ext <| Nat.zero_add _
+    (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by simp
 
 @[simp]
 theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :

src/Init/Data/List/Attach.lean

@@ -118,7 +118,6 @@ theorem attach_map_coe (l : List α) (f : α → β) :
 theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
   attach_map_coe _ _
 
-@[simp]
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
   (attach_map_coe _ _).trans (List.map_id _)
 
@@ -130,7 +129,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (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 : List α) (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l :=
   (attachWith_map_coe _ _ _).trans (List.map_id _)
@@ -174,8 +172,8 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by
   simp
 
-theorem pmap_eq_self {l : List α} {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 : List α} {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
   rw [pmap_eq_map_attach]
   conv => lhs; rhs; rw [← attach_map_subtype_val l]
   rw [map_inj_left]

src/Init/Data/List/Find.lean

@@ -566,7 +566,6 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
     | inl e => simpa [e, Fin.zero_eta, get_cons_zero]
     | inr e =>
       have ipm := Nat.succ_pred_eq_of_pos e
-      have ilt := Nat.le_trans ho (findIdx_le_length p)
       simp +singlePass only [← ipm, getElem_cons_succ]
       rw [← ipm, Nat.succ_lt_succ_iff] at h
       simpa using ih h

src/Init/Data/List/Lemmas.lean

@@ -216,7 +216,9 @@ We simplify `l[i]!` to `(l[i]?).getD default`.
 @[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (i : Nat) :
     l[i]! = (l[i]?).getD (default : α) := by
   simp only [getElem!_def]
-  split <;> simp_all
+  match l[i]? with
+  | some _ => simp
+  | none => simp
 
 /-! ### getElem? and getElem -/
 

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

@@ -68,8 +68,8 @@ theorem getElem?_modifyHead {l : List α} {f : α → α} {n} :
     (l.modifyHead f).drop n = l.drop n := by
   cases l <;> cases n <;> simp_all
 
-@[simp] theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
-    (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by cases l <;> simp
+theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
+    (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by simp
 
 @[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
     (l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all
@@ -142,7 +142,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (
 theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
     l.modifyHead f = l.modify f 0 := by cases l <;> simp
 
-@[simp] theorem modify_eq_nil_iff (f : α → α) (n) (l : List α) :
+@[simp] theorem modify_eq_nil_iff {f : α → α} {n} {l : List α} :
     l.modify f n = [] ↔ l = [] := by cases l <;> cases n <;> simp
 
 theorem getElem?_modify (f : α → α) :

src/Init/Data/List/Sort/Impl.lean

@@ -147,23 +147,21 @@ where
     mergeTR (run' r) (run l) le
 
 theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) :
-    (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by have := l.2; simp; omega⟩ := by
+    (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by
   simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_snd]
   congr
-  have := l.2
   omega
 theorem splitRevInTwo'_snd (l : { l : List α // l.length = n }) :
-    (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by have := l.2; simp; omega⟩ := by
+    (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by
   simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_fst, reverse_reverse]
   congr 2
-  have := l.2
   simp
   omega
 theorem splitRevInTwo_fst (l : { l : List α // l.length = n }) :
-    (splitRevInTwo l).1 = ⟨(splitInTwo l).1.1.reverse, by have := l.2; simp; omega⟩ := by
+    (splitRevInTwo l).1 = ⟨(splitInTwo l).1.1.reverse, by simp; omega⟩ := by
   simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_fst]
 theorem splitRevInTwo_snd (l : { l : List α // l.length = n }) :
-    (splitRevInTwo l).2 = ⟨(splitInTwo l).2.1, by have := l.2; simp; omega⟩ := by
+    (splitRevInTwo l).2 = ⟨(splitInTwo l).2.1, by simp; omega⟩ := by
   simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_snd]
 
 theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR.run le l = mergeSort l.1 le

src/Init/Data/List/Sort/Lemmas.lean

@@ -285,8 +285,6 @@ theorem sorted_mergeSort
   | [] => by simp [mergeSort]
   | [a] => by simp [mergeSort]
   | a :: b :: xs => by
-    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
-    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
     rw [mergeSort]
     apply sorted_merge @trans @total
     apply sorted_mergeSort trans total

src/Init/Data/List/ToArray.lean

@@ -38,7 +38,7 @@ theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
   simp
 
 @[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
-  cases l <;> simp
+  cases l <;> simp [Array.isEmpty]
 
 @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
 

src/Init/Data/Option/Attach.lean

@@ -56,7 +56,6 @@ theorem attach_map_val (o : Option α) (f : α → β) :
     (o.attach.map fun i => f i.val) = o.map f :=
   attach_map_coe _ _
 
-@[simp]
 theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
   (attach_map_coe _ _).trans (congrFun Option.map_id _)
@@ -69,12 +68,11 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
     ((o.attachWith p H).map fun i => f i.val) = o.map f :=
   attachWith_map_coe _ _ _
 
-@[simp]
 theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
 
-@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
+theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
   | none, ⟨x, h⟩ => by simp at h
   | some a, ⟨x, h⟩ => by simpa using h
 
@@ -92,14 +90,14 @@ theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a
     (o.attachWith p H).isSome = o.isSome := by
   cases o <;> simp
 
-@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by
+@[simp] theorem attach_eq_none_iff {o : Option α} : o.attach = none ↔ o = none := by
   cases o <;> simp
 
 @[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
     o.attach = some x ↔ o = some x.val := by
   cases o <;> cases x <;> simp
 
-@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+@[simp] theorem attachWith_eq_none_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) :
     o.attachWith p H = none ↔ o = none := by
   cases o <;> simp
 

src/Init/Data/Sum/Lemmas.lean

@@ -30,7 +30,7 @@ protected theorem «exists» {p : α ⊕ β → Prop} :
     | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
     | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
 
-theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) :
+theorem forall_sum {γ : α ⊕ β → Sort _} {p : (∀ ab, γ ab) → Prop} :
     (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
   refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
   have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by

src/Init/GetElem.lean

@@ -176,11 +176,14 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
   simp only [getElem?_def] at h ⊢
   split <;> simp_all
 
-@[simp] theorem isNone_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isNone = ¬dom c i := by
+@[simp] theorem getElem?_eq_none [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i := by
   simp only [getElem?_def]
   split <;> simp_all
 
+@[deprecated getElem?_eq_none (since := "2024-12-11")]
+abbrev isNone_getElem? := @getElem?_eq_none
+
 @[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by
   simp only [getElem?_def]

src/Init/SimpLemmas.lean

@@ -153,6 +153,7 @@ instance : Std.LawfulIdentity Or False where
 @[simp] theorem false_implies (p : Prop) : (False → p) = True := eq_true False.elim
 @[simp] theorem forall_false (p : False → Prop) : (∀ h : False, p h) = True := eq_true (False.elim ·)
 @[simp] theorem implies_true (α : Sort u) : (α → True) = True := eq_true fun _ => trivial
+-- This is later proved by the simp lemma `forall_const`, but this is useful during bootstrapping.
 @[simp] theorem true_implies (p : Prop) : (True → p) = p := propext ⟨(· trivial), (fun _ => ·)⟩
 @[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim
 @[simp] theorem not_true_eq_false : (¬ True) = False := by decide

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -830,9 +830,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
   simp_to_model using List.containsKey_eq_keys_contains.symm
 
 @[simp]
-theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
-  simp_to_model 
+  simp_to_model
   rw [List.containsKey_eq_keys_contains]
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :

src/Std/Data/DHashMap/Lemmas.lean

@@ -111,15 +111,11 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k
     a ∈ m.insert k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert
 
-@[simp]
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insert k v).contains k :=
-  Raw₀.contains_insert_self ⟨m.1, _⟩ m.2
+    (m.insert k v).contains k := by simp
 
-@[simp]
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    k ∈ m.insert k v := by
-  simp [mem_iff_contains, contains_insert_self]
+    k ∈ m.insert k v := by simp
 
 @[simp]
 theorem size_empty {c} : (empty c : DHashMap α β).size = 0 :=
@@ -959,13 +955,13 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   Raw₀.contains_keys ⟨m.1, _⟩ m.2
 
 @[simp]
-theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
-    k ∈ m.keys ↔ k ∈ m := by 
+theorem mem_keys [LawfulBEq α] {k : α} :
+    k ∈ m.keys ↔ k ∈ m := by
   rw [mem_iff_contains]
   exact Raw₀.mem_keys ⟨m.1, _⟩ m.2
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
-    m.keys.Pairwise (fun a b => (a == b) = false) := 
+    m.keys.Pairwise (fun a b => (a == b) = false) :=
   Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
 end Std.DHashMap

src/Std/Data/HashMap/Lemmas.lean

@@ -119,14 +119,11 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β}
     a ∈ m.insert k v → (k == a) = false → a ∈ m :=
   DHashMap.mem_of_mem_insert
 
-@[simp]
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    (m.insert k v).contains k :=
-  DHashMap.contains_insert_self
+    (m.insert k v).contains k := by simp
 
-@[simp]
-theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v :=
-  DHashMap.mem_insert_self
+theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v := by
+  simp
 
 @[simp]
 theorem size_empty {c} : (empty c : HashMap α β).size = 0 :=

src/Std/Data/HashSet/Lemmas.lean

@@ -122,13 +122,10 @@ theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.insert k → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
   DHashMap.mem_of_mem_insertIfNew'
 
-@[simp]
-theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α}  : (m.insert k).contains k :=
-  HashMap.contains_insertIfNew_self
+theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k := by
+  simp
 
-@[simp]
-theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k :=
-  HashMap.mem_insertIfNew_self
+theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp
 
 @[simp]
 theorem size_empty {c} : (empty c : HashSet α).size = 0 :=

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -494,7 +494,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                conv => rhs; rw [Array.size_toArray]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
@@ -527,7 +527,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                conv => rhs; rw [Array.size_toArray]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
@@ -587,7 +587,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                conv => rhs; rw [Array.size_toArray]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -1115,11 +1115,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
     simp [li, Array.getElem_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2
-    simp only [derivedLits_arr_def, Array.size_mk] at i_property
+    simp only [derivedLits_arr_def, Array.size_toArray] at i_property
     exact i_property
   have j_in_bounds : j.1 < derivedLits.length := by
     have j_property := j.2
-    simp only [derivedLits_arr_def, Array.size_mk] at j_property
+    simp only [derivedLits_arr_def, Array.size_toArray] at j_property
     exact j_property
   rcases derivedLits_satisfies_invariant ⟨li.1.1, li.1.2.2⟩ with ⟨_, h2⟩ | ⟨k, _, _, _, h3⟩ |
     ⟨k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3⟩
@@ -1216,7 +1216,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
       exact h2 derivedLits_arr[j] idx_in_list
   · apply Or.inr ∘ Or.inl
     have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by
-      simp only [derivedLits_arr_def, Array.size_mk]
+      simp only [derivedLits_arr_def, Array.size_toArray]
       exact j.2
     have i_gt_zero : i.1 > 0 := by rw [← j_eq_i]; exact (List.get derivedLits j).1.2.1
     refine ⟨⟨j.1, j_lt_derivedLits_arr_size⟩, List.get derivedLits j |>.2, i_gt_zero, ?_⟩
@@ -1229,7 +1229,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
         intro k _ k_ne_j
         have k_in_bounds : k < derivedLits.length := by
           have k_property := k.2
-          simp only [derivedLits_arr_def, Array.size_mk] at k_property
+          simp only [derivedLits_arr_def, Array.size_toArray] at k_property
           exact k_property
         have k_ne_j : ⟨k.1, k_in_bounds⟩ ≠ j := by
           apply Fin.ne_of_val_ne
@@ -1239,10 +1239,10 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
   · apply Or.inr ∘ Or.inr
     have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
-      simp only [derivedLits_arr_def, Array.size_mk]
+      simp only [derivedLits_arr_def, Array.size_toArray]
       exact j1.2
     have j2_lt_derivedLits_arr_size : j2.1 < derivedLits_arr.size := by
-      simp only [derivedLits_arr_def, Array.size_mk]
+      simp only [derivedLits_arr_def, Array.size_toArray]
       exact j2.2
     have i_gt_zero : i.1 > 0 := by rw [← j1_eq_i]; exact (List.get derivedLits j1).1.2.1
     refine ⟨⟨j1.1, j1_lt_derivedLits_arr_size⟩,
@@ -1260,7 +1260,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
         intro k _ k_ne_j1 k_ne_j2
         have k_in_bounds : k < derivedLits.length := by
           have k_property := k.2
-          simp only [derivedLits_arr_def, Array.size_mk] at k_property
+          simp only [derivedLits_arr_def, Array.size_toArray] at k_property
           exact k_property
         have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
           apply Fin.ne_of_val_ne

tests/lean/run/array_simp.lean

@@ -6,6 +6,9 @@
 #check_simp #[1,2,3,4,5][7]! ~> (default : Nat)
 #check_simp (#[] : Array Nat)[0]! ~> (default : Nat)
 
+variable {xs : Array α} in
+#check_simp xs.size = 0 ~> xs = #[]
+
 attribute [local simp] Id.run in
 #check_simp
   (Id.run do