comment

building upon #3714, this (almost) implements the second half of #3302.

The main effect is that we now get a better error message when `rfl`
fails. For
```lean
example : n+1+m = n + (1+m) := by rfl
```
instead of the wall of text
```
The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```
we now get
```
error: tactic 'rfl' failed, the left-hand side
  n + 1 + m
is not definitionally equal to the right-hand side
  n + (1 + m)
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```

Unfortunately, because of very subtle differences in semantics (which
transparency setting is used when reducing the goal and whether the
“implicit lambda” feature applies) I could not make this simply the only
`rfl` implementation. So `rfl` remains a macro and is still expanded to
`eq_refl` (difference transparency setting) and `exact Iff.rfl` and
`exact HEq.rfl` (implicit lambda) to not break existing code. This can
be revised later, so this still closes: #3302.

A user might still be puzzled *why* to terms are not defeq. Explaining
that better (“reduced to… and reduces to… etc.”) would also be great,
but that’s not specific to `rfl`, so better left for some other time.

src/Init/Control/Lawful/Basic.lean

@@ -33,6 +33,10 @@ attribute [simp] id_map
 @[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
   id_map x
 
+@[simp] theorem Functor.map_map [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) :
+    g <$> m <$> x = (fun a => g (m a)) <$> x :=
+  (comp_map _ _ _).symm
+
 /--
 The `Applicative` typeclass only contains the operations of an applicative functor.
 `LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor:
@@ -83,12 +87,16 @@ class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m
   seq_assoc x g h := (by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind])
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
-attribute [simp] pure_bind bind_assoc
+attribute [simp] pure_bind bind_assoc bind_pure_comp
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   show x >>= (fun a => pure (id a)) = x
   rw [bind_pure_comp, id_map]
 
+/--
+Use `simp [← bind_pure_comp]` rather than `simp [map_eq_pure_bind]`,
+as `bind_pure_comp` is in the default simp set, so also using `map_eq_pure_bind` would cause a loop.
+-/
 theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
   rw [← bind_pure_comp]
 
@@ -109,10 +117,21 @@ theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α →
 
 theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
   rw [seqRight_eq]
-  simp [map_eq_pure_bind, seq_eq_bind_map, const]
+  simp only [map_eq_pure_bind, const, seq_eq_bind_map, bind_assoc, pure_bind, id_eq, bind_pure]
 
 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
-  rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
+  rw [seqLeft_eq]
+  simp only [map_eq_pure_bind, seq_eq_bind_map, bind_assoc, pure_bind, const_apply]
+
+@[simp] theorem map_bind [Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) :
+    f <$> (x >>= g) = x >>= fun a => f <$> g a := by
+  rw [← bind_pure_comp, LawfulMonad.bind_assoc]
+  simp [bind_pure_comp]
+
+@[simp] theorem bind_map_left [Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) :
+    ((f <$> x) >>= fun b => g b) = (x >>= fun a => g (f a)) := by
+  rw [← bind_pure_comp]
+  simp only [bind_assoc, pure_bind]
 
 /--
 An alternative constructor for `LawfulMonad` which has more

src/Init/Control/Lawful/Instances.lean

@@ -25,7 +25,7 @@ theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
 @[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
 
 @[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
-  simp[ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont, map_eq_pure_bind]
+  simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
 
 @[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
   simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
@@ -43,7 +43,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
 
 @[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
     : (f <$> x).run = Except.map f <$> x.run := by
-  simp [Functor.map, ExceptT.map, map_eq_pure_bind]
+  simp [Functor.map, ExceptT.map, ←bind_pure_comp]
   apply bind_congr
   intro a; cases a <;> simp [Except.map]
 
@@ -62,7 +62,7 @@ protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad
   intro
   | Except.error _ => simp
   | Except.ok _ =>
-    simp [map_eq_pure_bind]; apply bind_congr; intro b;
+    simp [←bind_pure_comp]; apply bind_congr; intro b;
     cases b <;> simp [comp, Except.map, const]
 
 protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
@@ -175,7 +175,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   simp [bind, StateT.bind, run]
 
 @[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
-  simp [Functor.map, StateT.map, run, map_eq_pure_bind]
+  simp [Functor.map, StateT.map, run, ←bind_pure_comp]
 
 @[simp] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
 
@@ -210,13 +210,13 @@ theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f :
 
 theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by
   apply ext; intro s
-  simp [map_eq_pure_bind, const]
+  simp [←bind_pure_comp, const]
   apply bind_congr; intro p; cases p
   simp [Prod.eta]
 
 theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y := by
   apply ext; intro s
-  simp [map_eq_pure_bind]
+  simp [←bind_pure_comp]
 
 instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   id_map         := by intros; apply ext; intros; simp[Prod.eta]
@@ -224,7 +224,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   seqLeft_eq     := seqLeft_eq
   seqRight_eq    := seqRight_eq
   pure_seq       := by intros; apply ext; intros; simp
-  bind_pure_comp := by intros; apply ext; intros; simp; apply LawfulMonad.bind_pure_comp
+  bind_pure_comp := by intros; apply ext; intros; simp
   bind_map       := by intros; rfl
   pure_bind      := by intros; apply ext; intros; simp
   bind_assoc     := by intros; apply ext; intros; simp

src/Init/Core.lean

@@ -823,6 +823,7 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+-- And, also for backward compatibility, we try `Iff.rfl.` using `exact` (see #5366)
 macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
 
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
@@ -837,6 +838,9 @@ instance : Trans Iff Iff Iff where
 theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
 theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
+theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm
+theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
+
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
 theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm
@@ -1382,11 +1386,6 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
-/-- Replacement for `Array.mk.injEq`; we avoid mentioning the constructor and prefer `List.toArray`. -/
-abbrev List.toArray_inj := @Array.mk.injEq
-
-attribute [deprecated List.toArray_inj (since := "2024-09-09")] Array.mk.injEq
-
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
 

src/Init/Data/Array/Basic.lean

@@ -73,8 +73,7 @@ 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 := by
-  simp [List.toArray, Array.mkEmpty]
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 

src/Init/Data/Array/BasicAux.lean

@@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
 import Init.NotationExtra
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
-  simp only [push, List.toArray_inj] at h
+  simp only [push, mk.injEq] at h
   have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h
   cases as; cases bs
   simp_all
@@ -34,7 +34,7 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
 
 @[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
   apply propext; apply Iff.intro
-  · intro h; simp [toArray] at h; have := of_toArrayAux_eq_toArrayAux h rfl; exact this.1
+  · intro h; simpa [toArray] using h
   · intro h; rw [h]
 
 def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=

src/Init/Data/Array/Lemmas.lean

@@ -19,20 +19,37 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-/-- We avoid mentioning the constructor `Array.mk` directly, preferring `List.toArray`. -/
-@[simp] theorem mk_eq_toArray (as : List α) : Array.mk as = as.toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
-theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
+theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
   by_cases i < a.size <;> (try simp [*]) <;> rfl
 
+theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
+  getElem?_pos ..
+
+@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
+  by_cases h : i < a.size
+  · simp [getElem?_eq_getElem, h]
+  · rw [getElem?_neg a i h]
+    simp_all
+
+theorem getElem?_eq {a : Array α} {i : Nat} :
+    a[i]? = if h : i < a.size then some a[i] else none := by
+  split
+  · simp_all [getElem?_eq_getElem]
+  · simp_all
+
+theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
+  rw [getElem?_eq]
+  split <;> simp_all
+
+@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
+abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
+
 @[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
-abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
+abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
 
 @[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
 theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
@@ -41,11 +58,11 @@ theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
-  simp only [push, getElem_eq_toList_getElem, List.concat_eq_append, List.getElem_append_left, h]
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
 @[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
-  simp only [push, getElem_eq_toList_getElem, List.concat_eq_append]
-  rw [List.getElem_append_right] <;> simp [getElem_eq_toList_getElem, Nat.zero_lt_one]
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
+  rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
 
 theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
@@ -62,26 +79,40 @@ open Array
 
 /-! ### Lemmas about `List.toArray`. -/
 
-@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
-
-@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
+@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
-@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
-  | ⟨l⟩ => ext' (toList_toArray l)
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
 
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
-    a.toArray[i] = a[i]'(by simpa using h) := by
-  have h₁ := mk_eq_toArray a
-  have h₂ := getElem_mk (by simpa using h)
-  simpa [h₁] using h₂
+    a.toArray[i] = a[i]'(by simpa using h) := rfl
 
 @[simp] theorem toArray_concat {as : List α} {x : α} :
     (as ++ [x]).toArray = as.toArray.push x := by
   apply ext'
   simp
 
+@[simp] theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
+    l.toArray.foldrM f init = l.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+@[simp] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
+    l.toArray.foldlM f init = l.foldlM f init := by
+  rw [foldlM_eq_foldlM_toList]
+
+@[simp] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
+    l.toArray.foldr f init = l.foldr f init := by
+  rw [foldr_eq_foldr_toList]
+
+@[simp] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
+    l.toArray.foldl f init = l.foldl f init := by
+  rw [foldl_eq_foldl_toList]
+
 end List
 
 namespace Array
@@ -90,10 +121,10 @@ attribute [simp] uset
 
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
-@[deprecated List.toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @List.toArray_toList
-@[deprecated List.toArray_toList (since := "2024-09-09")]
-abbrev toArray_toList := @List.toArray_toList
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
 
 @[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
 
@@ -228,11 +259,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
-  simp [set, getElem_eq_toList_getElem, ←eq]
+  simp [set, getElem_eq_getElem_toList, ←eq]
 
 @[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
     (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
-  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
+  simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
@@ -322,7 +353,7 @@ termination_by n - i
 abbrev mkArray_data := @toList_mkArray
 
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [Array.getElem_eq_toList_getElem]
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 
 /-- # mem -/
 
@@ -363,7 +394,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
   hidx
 
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
-  erw [Array.mem_def, getElem_eq_toList_getElem]
+  erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
 theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
@@ -374,14 +405,11 @@ abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
 
-theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = some a[i] :=
-  getElem?_pos ..
-
 theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_neg, h]
 
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
-  simp only [getElem_eq_toList_getElem, List.getElem_mem]
+  simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
 @[deprecated getElem_mem_toList (since := "2024-09-09")]
 abbrev getElem_mem_data := @getElem_mem_toList
@@ -441,7 +469,7 @@ abbrev data_set := @toList_set
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1] = v := by
-  simp only [set, getElem_eq_toList_getElem, List.getElem_set_self]
+  simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
 theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@@ -460,7 +488,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
 
 @[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
     (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
-  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
+  simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
   (setD a i v)[i] = v := by
@@ -476,7 +504,7 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
     a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
   simp [swap, fin_cast_val]
 
-theorem toList_swap (a : Array α) (i j : Fin a.size) :
+@[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
     (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
 
 @[deprecated toList_swap (since := "2024-09-09")]
@@ -489,7 +517,7 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]?
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
 
--- @[simp] -- FIXME: gives a weird linter error
+@[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
 
@@ -562,7 +590,7 @@ abbrev data_range := @toList_range
 
 @[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
-  simp [getElem_eq_toList_getElem]
+  simp [getElem_eq_getElem_toList]
 
 set_option linter.deprecated false in
 @[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
@@ -608,6 +636,32 @@ set_option linter.deprecated false in
 
 /-! ### foldl / foldr -/
 
+@[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
+    foldlM.loop f #[] s h i j init = pure init := by
+  unfold foldlM.loop; split
+  · split
+    · rfl
+    · simp at h
+      omega
+  · rfl
+
+@[simp] theorem foldlM_empty [Monad m] (f : β → α → m β) (init : β) :
+    foldlM f init #[] start stop = return init := by
+  simp [foldlM]
+
+@[simp] theorem foldrM_fold_empty [Monad m] (f : α → β → m β) (init : β) (i j : Nat) (h) :
+    foldrM.fold f #[] i j h init = pure init := by
+  unfold foldrM.fold
+  split <;> rename_i h₁
+  · rfl
+  · split <;> rename_i h₂
+    · rfl
+    · simp at h₂
+
+@[simp] theorem foldrM_empty [Monad m] (f : α → β → m β) (init : β) :
+    foldrM f init #[] start stop = return init := by
+  simp [foldrM]
+
 -- This proof is the pure version of `Array.SatisfiesM_foldlM`,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldl_induction
@@ -647,12 +701,12 @@ theorem foldr_induction
   simp only [mem_def, map_toList, List.mem_map]
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return (← arr.toList.mapM f).toArray := by
+    arr.mapM f = return mk (← arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
-  | cons a l ih => simp [ih]; simp [map_eq_pure_bind]
+  | cons a l ih => simp [ih]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
@@ -793,7 +847,7 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
 
 /-! ### filter -/
 
-@[simp] theorem filter_toList (p : α → Bool) (l : Array α) :
+@[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
   rw [foldl_eq_foldl_toList]
@@ -804,23 +858,23 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
   induction l with simp
   | cons => split <;> simp [*]
 
-@[deprecated filter_toList (since := "2024-09-09")]
-abbrev filter_data := @filter_toList
+@[deprecated toList_filter (since := "2024-09-09")]
+abbrev filter_data := @toList_filter
 
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
-  simp only [filter_toList, List.filter_filter]
+  simp only [toList_filter, List.filter_filter]
 
 @[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
-  simp only [mem_def, filter_toList, List.mem_filter]
+  simp only [mem_def, toList_filter, List.mem_filter]
 
 theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   (mem_filter.mp h).1
 
 /-! ### filterMap -/
 
-@[simp] theorem filterMap_toList (f : α → Option β) (l : Array α) :
+@[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
   rw [foldlM_eq_foldlM_toList]
@@ -833,12 +887,12 @@ theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
-@[deprecated filterMap_toList (since := "2024-09-09")]
-abbrev filterMap_data := @filterMap_toList
+@[deprecated toList_filterMap (since := "2024-09-09")]
+abbrev filterMap_data := @toList_filterMap
 
 @[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
-  simp only [mem_def, filterMap_toList, List.mem_filterMap]
+  simp only [mem_def, toList_filterMap, List.mem_filterMap]
 
 /-! ### empty -/
 
@@ -861,7 +915,7 @@ theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size :=
 
 theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
     (as ++ bs)[i] = as[i] := by
-  simp only [getElem_eq_toList_getElem]
+  simp only [getElem_eq_getElem_toList]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [append_toList]
@@ -869,7 +923,7 @@ theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i <
 theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
-  simp only [getElem_eq_toList_getElem]
+  simp only [getElem_eq_getElem_toList]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [append_toList]
@@ -1017,6 +1071,33 @@ theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : a
 
 /-! ### any -/
 
+theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) :
+    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) = anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
+  rw [anyM.loop]
+  conv => rhs; rw [anyM.loop]
+  split <;> rename_i h'
+  · simp only [Nat.add_lt_add_iff_right] at h'
+    rw [dif_pos h']
+    rw [anyM_loop_cons]
+    simp
+  · rw [dif_neg]
+    omega
+
+@[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (as : Array α) :
+    as.toList.anyM p = as.anyM p :=
+  match as with
+  | ⟨[]⟩  => rfl
+  | ⟨a :: as⟩ => by
+    simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
+    rw [anyM.loop, dif_pos (by omega)]
+    congr 1
+    funext b
+    split
+    · simp
+    · simp only [Bool.false_eq_true, ↓reduceIte]
+      rw [anyM_loop_cons]
+      simpa [anyM] using anyM_toList p ⟨as⟩
+
 -- Auxiliary for `any_iff_exists`.
 theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
     anyM.loop (m := Id) p as stop h start = true ↔
@@ -1061,6 +1142,17 @@ theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p :
 
 /-! ### all -/
 
+theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
+  dsimp [allM, anyM]
+  simp
+
+@[simp] theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    as.toList.allM p = as.allM p := by
+  rw [allM_eq_not_anyM_not]
+  rw [← anyM_toList]
+  rw [List.allM_eq_not_anyM_not]
+
 theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
     all as p start stop = !(any as (!p ·) start stop) := by
   dsimp [all, allM]
@@ -1082,10 +1174,10 @@ theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p :
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
   constructor
   · rintro w x ⟨r, h, rfl⟩
-    rw [← getElem_eq_toList_getElem]
+    rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
   · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_toList_getElem as i.2).symm⟩
+    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
 
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [all_def, List.all_eq_true, mem_def]
@@ -1157,3 +1249,117 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
 
 end Array
+
+
+open Array
+
+namespace List
+
+/-!
+### More theorems about `List.toArray`, followed by an `Array` operation.
+
+Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
+-/
+
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
+@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
+  simp [getElem?_eq_getElem?_toList]
+
+@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
+  simp
+
+@[simp] theorem push_append_toArray (as : Array α) (a : α) (l : List α) :
+    as.push a ++ l.toArray = as ++ (a :: l).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
+    l.toArray.mapM f = List.toArray <$> l.mapM f := by
+  simp only [← mapM'_eq_mapM, mapM_eq_foldlM]
+  suffices ∀ init : Array β,
+      foldlM (fun bs a => bs.push <$> f a) init l.toArray = (init ++ toArray ·) <$> mapM' f l by
+    simpa using this #[]
+  intro init
+  induction l generalizing init with
+  | nil => simp
+  | cons a l ih =>
+    simp only [foldlM_toArray] at ih
+    rw [size_toArray, mapM'_cons, foldlM_toArray]
+    simp [ih]
+
+@[simp] theorem map_toArray (f : α → β) (l : List α) : l.toArray.map f = (l.map f).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem set_toArray (l : List α) (i : Fin l.toArray.size) (a : α) :
+    l.toArray.set i a = (l.set i a).toArray := by
+  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
+
+@[simp] theorem setD_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setD i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setD]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
+@[simp] theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+@[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [Array.any_def]
+
+@[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+@[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [Array.all_def]
+
+@[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
+    l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem filter_toArray (p : α → Bool) (l : List α) :
+    l.toArray.filter p = (l.filter p).toArray := by
+  apply ext'
+  erw [toList_filter] -- `erw` required to unify `l.length` with `l.toArray.size`.
+
+@[simp] theorem filterMap_toArray (f : α → Option β) (l : List α) :
+    l.toArray.filterMap f = (l.filterMap f).toArray := by
+  apply ext'
+  erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
+
+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
+  apply ext'
+  simp
+
+end List

src/Init/Data/Array/TakeDrop.lean

@@ -12,7 +12,7 @@ namespace Array
 theorem exists_of_uset (self : Array α) (i d h) :
     ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.uset i d h).toList = l₁ ++ d :: l₂ := by
-  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
+  simpa only [ugetElem_eq_getElem, getElem_eq_getElem_toList, uset, toList_set] using
     List.exists_of_set _
 
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -11,6 +11,7 @@ import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Data.Int.Pow
 
 set_option linter.missingDocs true
 
@@ -271,6 +272,10 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
 
+@[simp] theorem toNat_mod_cancel' {x : BitVec n} :
+    (x.toNat : Int) % (((2 ^ n) : Nat) : Int) = x.toNat := by
+  rw_mod_cast [toNat_mod_cancel]
+
 @[simp] theorem sub_toNat_mod_cancel {x : BitVec w} (h : ¬ x = 0#w) :
     (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
   simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h
@@ -927,6 +932,10 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
+@[simp] theorem not_allOnes : ~~~ allOnes w = 0#w := by
+  ext
+  simp
+
 @[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
   ext i
   simp
@@ -935,6 +944,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext i
   simp
 
+@[simp]
+theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
+  ext i
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -1068,6 +1082,16 @@ theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
   cases h₅ : decide (i < n + m) <;>
     simp at * <;> omega
 
+@[simp]
+theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} {n : Nat} :
+    BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by
+  simp [← BitVec.shiftLeft_and_distrib]
+
+@[simp]
+theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
+    BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
+  simp [← shiftLeft_or_distrib]
+
 @[deprecated shiftLeft_add (since := "2024-06-02")]
 theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
     (x <<< n) <<< m = x <<< (n + m) := by
@@ -1410,6 +1434,10 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   rw [getLsbD_append]
   simpa using lt_of_getLsbD
 
+@[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
+  ext
+  simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
+
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = x ++ cast (by omega) y := by
   ext
@@ -1655,6 +1683,10 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
+@[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
+  ext
+  simp [getLsbD_concat]
+
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -1744,6 +1776,21 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 @[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
   simp [Neg.neg, BitVec.neg]
 
+theorem toInt_neg {x : BitVec w} :
+    (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
+  simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
+  rw [← Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
+    Int.bmod_add_cancel]
+  by_cases h : x.toNat < ((2 ^ w) + 1) / 2
+  · rw [Int.bmod_pos (x := x.toNat)]
+    all_goals simp [toNat_mod_cancel', h]
+    norm_cast
+  · rw [Int.bmod_neg (x := x.toNat)]
+    · simp only [toNat_mod_cancel']
+      rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
+    · norm_cast
+      simp_all
+
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
   rfl
@@ -2166,6 +2213,20 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
 theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
   rw [← twoPow_zero, getLsbD_twoPow]
 
+@[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by
+  ext
+  simp [getLsbD_cons]
+  omega
+
+@[simp] theorem false_cons_zero : cons false 0#w = 0#(w + 1) := by
+  ext
+  simp [getLsbD_cons]
+
+@[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
+  ext
+  simp [getLsbD_concat]
+  omega
+
 /- ### setWidth, setWidth, and bitwise operations -/
 
 /--
@@ -2258,10 +2319,28 @@ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) :=
   simp only [intMin, getLsbD_twoPow, boolToPropSimps]
   omega
 
+/--
+The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
+-/
 @[simp, bv_toNat]
 theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
   simp [intMin]
 
+/--
+The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
+-/
+@[simp]
+theorem toInt_intMin {w : Nat} :
+    (intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat) := by
+  by_cases h : w = 0
+  · subst h
+    simp [BitVec.toInt]
+  · have w_pos : 0 < w := by omega
+    simp only [BitVec.toInt, toNat_intMin, w_pos, Nat.two_pow_pred_mod_two_pow,
+      Int.two_pow_pred_sub_two_pow, ite_eq_right_iff]
+    rw [Nat.mul_comm]
+    simp [w_pos]
+
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   by_cases h : 0 < w
@@ -2269,6 +2348,22 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   · simp only [Nat.not_lt, Nat.le_zero_eq] at h
     simp [bv_toNat, h]
 
+theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
+    (-x).toInt = -(x.toInt) := by
+  simp only [ne_eq, toNat_eq, toNat_intMin] at rs
+  by_cases x_zero : x = 0
+  · subst x_zero
+    simp [BitVec.toInt]
+    omega
+  by_cases w_0 : w = 0
+  · subst w_0
+    simp [BitVec.eq_nil x]
+  have : 0 < w := by omega
+  rw [Nat.two_pow_pred_mod_two_pow (by omega)] at rs
+  simp only [BitVec.toInt, BitVec.toNat_neg, BitVec.sub_toNat_mod_cancel x_zero]
+  have := @Nat.two_pow_pred_mul_two w (by omega)
+  split <;> split <;> omega
+
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/

src/Init/Data/Int/Pow.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 -/
 prelude
 import Init.Data.Int.Lemmas
+import Init.Data.Nat.Lemmas
 
 namespace Int
 
@@ -35,10 +36,24 @@ theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤
 theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   pow_le_pow_of_le_right h (Nat.zero_le _)
 
+@[norm_cast]
 theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
   match n with
   | 0 => rfl
   | n + 1 =>
     simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
 
+@[simp]
+protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
+    ((2 ^ (w - 1) : Nat) - (2 ^ w : Nat) : Int) = - ((2 ^ (w - 1) : Nat) : Int) := by
+  rw [← Nat.two_pow_pred_add_two_pow_pred h]
+  omega
+
+@[simp]
+protected theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) :
+    (2 : Int) ^ (w - 1) - (2 : Int) ^ w = - (2 : Int) ^ (w - 1) := by
+  norm_cast
+  rw [← Nat.two_pow_pred_add_two_pow_pred h]
+  simp [h]
+
 end Int

src/Init/Data/List/Lemmas.lean

@@ -1654,6 +1654,11 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 
 /-! ### append -/
 
+@[simp] theorem nil_append_fun : (([] : List α) ++ ·) = id := rfl
+
+@[simp] theorem cons_append_fun (a : α) (as : List α) :
+    (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
+
 theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h) :
     (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
   split <;> rename_i h'
@@ -2392,6 +2397,12 @@ theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
 theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.length b :=
   map_const l b
 
+@[simp] theorem set_replicate_self : (replicate n a).set i a = replicate n a := by
+  apply ext_getElem
+  · simp
+  · intro i h₁ h₂
+    simp [getElem_set]
+
 @[simp] theorem append_replicate_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [eq_replicate_iff]
   constructor

src/Init/Data/List/Monadic.lean

@@ -51,6 +51,27 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
+/-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`. -/
+theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] (f : α → m β) (as : List α) (b : β) (bs : List β) :
+    (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
+      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc) := by
+  induction as generalizing b bs with
+  | nil => simp
+  | cons a as ih =>
+    simp only [bind_pure_comp] at ih
+    simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]
+
+theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
+    mapM f l = reverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) []) := by
+  rw [← mapM'_eq_mapM]
+  induction l with
+  | nil => simp
+  | cons a as ih =>
+    simp only [mapM'_cons, ih, bind_map_left, foldlM_cons, LawfulMonad.bind_assoc, pure_bind,
+      foldlM_cons_eq_append, _root_.map_bind, Functor.map_map, Function.comp_def, reverse_append,
+      reverse_cons, reverse_nil, nil_append, singleton_append]
+    simp [bind_pure_comp]
+
 /-! ### forM -/
 
 -- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
@@ -66,4 +87,16 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
     (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
   induction l₁ <;> simp [*]
 
+/-! ### allM -/
+
+theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
+    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    simp only [allM, anyM, bind_map_left, _root_.map_bind]
+    congr
+    funext b
+    split <;> simp_all
+
 end List

src/Init/Data/Nat/Lemmas.lean

@@ -767,6 +767,11 @@ protected theorem two_pow_pred_mod_two_pow (h : 0 < w) :
   rw [mod_eq_of_lt]
   apply Nat.pow_pred_lt_pow (by omega) h
 
+@[simp]
+theorem two_pow_pred_mul_two (h : 0 < w) :
+    2 ^ (w - 1) * 2 = 2 ^ w := by
+  simp [← Nat.pow_succ, Nat.sub_add_cancel h]
+
 /-! ### log2 -/
 
 @[simp]

src/Init/Data/Repr.lean

@@ -163,7 +163,7 @@ protected def _root_.USize.repr (n : @& USize) : String :=
 
 /-- We statically allocate and memoize reprs for small natural numbers. -/
 private def reprArray : Array String := Id.run do
-  List.range 128 |>.map (·.toUSize.repr) |> List.toArray
+  List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
   if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else

src/Init/Prelude.lean

@@ -754,10 +754,10 @@ infer the proof of `Nonempty α`.
 noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
   Classical.choice inferInstance
 
-instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
+instance {α : Sort u} {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
-instance Pi.instNonempty (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] :
+instance Pi.instNonempty {α : Sort u} {β : α → Sort v} [(a : α) → Nonempty (β a)] :
     Nonempty ((a : α) → β a) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
@@ -767,7 +767,7 @@ instance : Inhabited (Sort u) where
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => default
 
-instance Pi.instInhabited (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] :
+instance Pi.instInhabited {α : Sort u} {β : α → Sort v} [(a : α) → Inhabited (β a)] :
     Inhabited ((a : α) → β a) where
   default := fun _ => default
 
@@ -2570,7 +2570,9 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
+  You can also use the synonym `List.toArray` when dot notation is convenient.
+
+  At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
   list.
   -/
   mk ::
@@ -2584,6 +2586,9 @@ structure Array (α : Type u) where
 attribute [extern "lean_array_to_list"] Array.toList
 attribute [extern "lean_array_mk"] Array.mk
 
+@[inherit_doc Array.mk, match_pattern]
+abbrev List.toArray (xs : List α) : Array α := .mk xs
+
 /-- Construct a new empty array with initial capacity `c`. -/
 @[extern "lean_mk_empty_array_with_capacity"]
 def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
@@ -2730,7 +2735,7 @@ def List.redLength : List α → Nat
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
 @[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArray (as : List α) : Array α :=
+def List.toArrayImpl (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/

src/Init/Tactics.lean

@@ -149,26 +149,27 @@ syntax (name := assumption) "assumption" : tactic
 
 /--
 `contradiction` closes the main goal if its hypotheses are "trivially contradictory".
+
 - Inductive type/family with no applicable constructors
-```lean
-example (h : False) : p := by contradiction
-```
+  ```lean
+  example (h : False) : p := by contradiction
+  ```
 - Injectivity of constructors
-```lean
-example (h : none = some true) : p := by contradiction  --
-```
+  ```lean
+  example (h : none = some true) : p := by contradiction  --
+  ```
 - Decidable false proposition
-```lean
-example (h : 2 + 2 = 3) : p := by contradiction
-```
+  ```lean
+  example (h : 2 + 2 = 3) : p := by contradiction
+  ```
 - Contradictory hypotheses
-```lean
-example (h : p) (h' : ¬ p) : q := by contradiction
-```
+  ```lean
+  example (h : p) (h' : ¬ p) : q := by contradiction
+  ```
 - Other simple contradictions such as
-```lean
-example (x : Nat) (h : x ≠ x) : p := by contradiction
-```
+  ```lean
+  example (x : Nat) (h : x ≠ x) : p := by contradiction
+  ```
 -/
 syntax (name := contradiction) "contradiction" : tactic
 
@@ -363,31 +364,24 @@ syntax (name := fail) "fail" (ppSpace str)? : tactic
 syntax (name := eqRefl) "eq_refl" : tactic
 
 /--
-`rfl` tries to close the current goal using reflexivity.
-This is supposed to be an extensible tactic and users can add their own support
-for new reflexive relations.
-
-Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
-reflexivity theorems (e.g., `Iff.rfl`).
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is equality, heterogeneous equality or any relation that
+has a reflexivity lemma tagged with the attribute @[refl].
 -/
-macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.")
-
-macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
-macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
+syntax "rfl" : tactic
 
 /--
-This tactic applies to a goal whose target has the form `x ~ x`,
-where `~` is a reflexive relation other than `=`,
-that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
+The same as `rfl`, but without trying `eq_refl` at the end.
 -/
 syntax (name := applyRfl) "apply_rfl" : tactic
 
+-- We try `apply_rfl` first, beause it produces a nice error message
 macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
 
+-- But, mostly for backward compatibility, we try `eq_refl` too (reduces more aggressively)
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
+-- Als for backward compatibility, because `exact` can trigger the implicit lambda feature (see #5366)
+macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -180,7 +180,7 @@ let _x.26 := @Array.push _ _x.24 z
 def foldArrayLiteral : Folder := fun args => do
   let #[_, .fvar fvarId] := args | return none
   let some (list, typ, level) ← getPseudoListLiteral fvarId | return none
-  let arr := list.toArray
+  let arr := Array.mk list
   let lit ← mkPseudoArrayLiteral arr typ level
   return some lit
 

src/Lean/Elab/Tactic/Rfl.lean

@@ -16,6 +16,10 @@ provided the reflexivity lemma has been marked as `@[refl]`.
 
 namespace Lean.Elab.Tactic.Rfl
 
+/--
+This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+-/
 @[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
   match stx with
   | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

src/Lean/Meta/Tactic/Rfl.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Newell Jensen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Newell Jensen, Thomas Murrills
+Authors: Newell Jensen, Thomas Murrills, Joachim Breitner
 -/
 prelude
 import Lean.Meta.Tactic.Apply
@@ -58,13 +58,13 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   -- NB: uses whnfR, we do not want to unfold the relation itself
   let t ← whnfR <|← instantiateMVars <|← goal.getType
   if t.getAppNumArgs < 2 then
-    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
+    throwTacticEx `rfl goal "expected goal to be a binary relation"
 
   -- Special case HEq here as it has a different argument order.
   if t.isAppOfArity ``HEq 4 then
     let gs ← goal.applyConst ``HEq.refl
     unless gs.isEmpty do
-      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+      throwTacticEx `rfl goal <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
         goalsToMessageData gs}"
     return
 
@@ -76,8 +76,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   unless success do
     let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
-      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
-    throwTacticEx `apply_rfl goal explanation
+      return m!"the left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
+    throwTacticEx `rfl goal explanation
 
   if rel.isAppOfArity `Eq 1 then
     -- The common case is equality: just use `Eq.refl`
@@ -86,6 +86,9 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
     goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
   else
     -- Else search through `@refl` keyed by the relation
+    -- We change the type to `lhs ~ lhs` so that we do not the (possibly costly) `lhs =?= rhs` check
+    -- again.
+    goal.setType (.app t.appFn! lhs)
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
@@ -102,7 +105,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
+      throwTacticEx `rfl goal m!"no @[refl] lemma registered for relation{indentExpr rel}"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

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

@@ -140,7 +140,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     refine ih.trans ?_
     simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
     rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
-      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem]
+      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList]
   · next i source target hi =>
     rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
     rwa [Array.size_eq_length_toList, Nat.not_lt] at hi

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -297,7 +297,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
       dsimp; omega
     rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
     simp only [List.get_eq_getElem, Nat.zero_add] at h
-    rw [← Array.getElem_eq_toList_getElem]
+    rw [← Array.getElem_eq_getElem_toList]
     simp [h]
   · have arr_data_length_le_i : arr.toList.length ≤ i := by
       dsimp; omega

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

@@ -503,7 +503,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq] at l_ne_b
@@ -536,7 +536,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               have i_eq_l : i = l.1 := by rw [← heq]
@@ -596,7 +596,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx] at heq
               simp only [Option.some.injEq] at heq
               rw [← heq] at hl

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

@@ -461,7 +461,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     constructor
     · rw [← Array.mem_toList]
       apply Array.getElem_mem_toList
-    · rw [← Array.getElem_eq_toList_getElem] at c'_in_f
+    · rw [← Array.getElem_eq_getElem_toList] at c'_in_f
       simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
         c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
       simpa [Clause.toList] using negPivot_in_c'
@@ -472,8 +472,8 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     dsimp at *
     omega
   simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
-  rw [← Array.getElem_eq_toList_getElem] at h'
-  rw [← Array.getElem_eq_toList_getElem] at c'_in_f
+  rw [← Array.getElem_eq_getElem_toList] at h'
+  rw [← Array.getElem_eq_getElem_toList] at c'_in_f
   exists ⟨j.1, j_in_bounds⟩
   simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
 

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

@@ -1140,25 +1140,25 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
       specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
       simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
       simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
-      simp only [List.get_eq_getElem, Array.getElem_eq_toList_getElem, not_true_eq_false] at h3
+      simp only [List.get_eq_getElem, Array.getElem_eq_getElem_toList, not_true_eq_false] at h3
     · next k_ne_i =>
       have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
       specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
       simp (config := { decide := true }) [Fin.getElem_fin, derivedLits_arr_def, ne_eq,
-        Array.getElem_eq_toList_getElem, li] at h3
+        Array.getElem_eq_getElem_toList, li] at h3
   · by_cases li.2 = true
     · next li_eq_true =>
       have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
         intro i_eq_k2
         rw [← i_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li] at li_eq_true
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li] at li_eq_true
       have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
         intro j_eq_k2
         rw [← j_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li_eq_lj, li] at li_eq_true
       by_cases ⟨i.1, i_in_bounds⟩ = k1
       · next i_eq_k1 =>
         have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
@@ -1167,11 +1167,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k1
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
       · next i_ne_k1 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
         apply h3
-        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_toList_getElem,
+        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_getElem_toList,
           ne_eq, derivedLits_arr_def, li]
         rfl
     · next li_eq_false =>
@@ -1180,13 +1180,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
         intro i_eq_k1
         rw [← i_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li] at li_eq_false
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li] at li_eq_false
       have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
         intro j_eq_k1
         rw [← j_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li_eq_lj, li] at li_eq_false
       by_cases ⟨i.1, i_in_bounds⟩ = k2
       · next i_eq_k2 =>
         have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
@@ -1195,10 +1195,10 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k2
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
       · next i_ne_k2 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
-        simp (config := { decide := true }) [Array.getElem_eq_toList_getElem, derivedLits_arr_def, li] at h3
+        simp (config := { decide := true }) [Array.getElem_eq_getElem_toList, derivedLits_arr_def, li] at h3
 
 theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormula n)
     (f_assignments_size : f.assignments.size = n)
@@ -1232,7 +1232,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
     constructor
     · apply Nat.zero_le
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j_eq_i]
         rfl
       · apply And.intro h1 ∘ And.intro h2
         intro k _ k_ne_j
@@ -1244,7 +1244,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j
-        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
         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
@@ -1258,11 +1258,11 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
             ⟨j2.1, j2_lt_derivedLits_arr_size⟩,
             i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
     constructor
-    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j1_eq_i]
+    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j1_eq_i]
       rw [← j1_eq_true]
       rfl
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j2_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j2_eq_i]
         rw [← j2_eq_false]
         rfl
       · apply And.intro h1 ∘ And.intro h2
@@ -1279,7 +1279,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j2
-        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
 
 theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -61,6 +61,8 @@ attribute [bv_normalize] BitVec.getLsbD_zero_length
 attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
+attribute [bv_normalize] BitVec.not_not
+
 
 end Constant
 
@@ -141,11 +143,6 @@ theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
 theorem BitVec.zero_mul (a : BitVec w) : 0#w * a = 0#w := by
   simp [bv_toNat]
 
-@[bv_normalize]
-theorem BitVec.not_not (a : BitVec w) : ~~~(~~~a) = a := by
-  ext
-  simp
-
 @[bv_normalize]
 theorem BitVec.shiftLeft_zero (n : BitVec w) : n <<< 0#w' = n := by
   ext i

src/lake/lakefile.toml

@@ -6,5 +6,5 @@ name = "Lake"
 
 [[lean_exe]]
 name = "lake"
-root = "Lake.Main"
+root = "LakeMain"
 supportInterpreter = true

src/util/shell.cpp

@@ -362,7 +362,7 @@ pair_ref<environment, object_ref> run_new_frontend(
     name const & main_module_name,
     uint32_t trust_level,
     optional<std::string> const & ilean_file_name,
-    uint8_t json
+    uint8_t json_output
 ) {
     object * oilean_file_name = mk_option_none();
     if (ilean_file_name) {

tests/lean/Process.lean

@@ -19,12 +19,6 @@ def usingIO {α} (x : IO α) : IO α := x
   discard $ child.wait;
   child.stdout.readToEnd
 
-#eval usingIO do
-  let child ← spawn { cmd := "true", stdin := Stdio.piped };
-  discard $ child.wait;
-  child.stdin.putStrLn "ha!";
-  child.stdin.flush <|> IO.println "flush of broken pipe failed"
-
 #eval usingIO do
   -- produce enough output to fill both pipes on all platforms
   let out ← output { cmd := "sh", args := #["-c", "printf '%100000s' >& 2; printf '%100001s'"] };

tests/lean/Process.lean.expected.out

@@ -2,7 +2,6 @@
 0
 "ho!\n"
 "hu!\n"
-flush of broken pipe failed
 100001
 100000
 0

tests/lean/run/4644.lean

@@ -11,11 +11,10 @@ def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
   sorted_from_var a 0
 
 /--
-error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+error: tactic 'rfl' failed, the left-hand side
+  check_sorted #[0, 3, 3, 5, 8, 10, 10, 10]
+is not definitionally equal to the right-hand side
+  true
 ⊢ check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true
 -/
 #guard_msgs in

tests/lean/run/do_eqv_proofs.lean

@@ -7,7 +7,7 @@ theorem ex1 [Monad m] [LawfulMonad m] (b : Bool) (ma : m α) (mb : α → m α)
     (ma >>= fun x => if b then mb x else pure x) := by
   cases b <;> simp
 
-attribute [simp] map_eq_pure_bind seq_eq_bind_map
+attribute [simp] seq_eq_bind_map
 
 theorem ex2 [Monad m] [LawfulMonad m] (b : Bool) (ma : m α) (mb : α → m α) (a : α) :
     (do let mut x ← ma

tests/lean/run/rflReducibility.lean

@@ -0,0 +1,25 @@
+/-!
+The (attribute-extensible) `rfl` tactic only unfolds the goal with reducible transparency to look
+for a relation which may have a `refl` lemma associated with it. But historically, `rfl` also
+invoked `eq_refl`, which more aggressively unfolds. This checks that this still works.
+-/
+
+def Foo (a b : Nat) : Prop := a = b
+
+/--
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+  Foo
+⊢ Foo 1 1
+-/
+#guard_msgs in
+example : Foo 1 1 := by
+  apply_rfl
+
+
+#guard_msgs in
+example : Foo 1 1 := by
+  eq_refl
+
+#guard_msgs in
+example : Foo 1 1 := by
+  rfl

tests/lean/run/rflTacticErrors.lean

@@ -9,11 +9,10 @@ This file tests the `rfl` tactic:
 -- First, let's see what `rfl` does:
 
 /--
-error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+error: tactic 'rfl' failed, the left-hand side
+  false
+is not definitionally equal to the right-hand side
+  true
 ⊢ false = true
 -/
 #guard_msgs in
@@ -28,9 +27,9 @@ attribute [refl] P.refl
 -- Plain error
 
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   42
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   23
 ⊢ P 42 23
 -/
@@ -42,9 +41,9 @@ example : P 42 23 := by apply_rfl
 opaque withImplicitNat {n : Nat} : Nat
 
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   @withImplicitNat 42
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   @withImplicitNat 23
 ⊢ P withImplicitNat withImplicitNat
 -/
@@ -86,13 +85,15 @@ example : True ↔ True   := by apply_rfl
 example : P true true   := by apply_rfl
 example : Q true true   := by apply_rfl
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   Q'
+⊢ Q' true true
 -/
 #guard_msgs in example : Q' true true  := by apply_rfl -- Error
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   R
+⊢ R true true
 -/
 #guard_msgs in example : R true true   := by apply_rfl -- Error
 
@@ -102,14 +103,16 @@ example : True ↔ True   := by with_reducible apply_rfl
 example : P true true   := by with_reducible apply_rfl
 example : Q true true   := by with_reducible apply_rfl
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   Q'
+⊢ Q' true true
 -/
 #guard_msgs in
 example : Q' true true  := by with_reducible apply_rfl -- Error
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   R
+⊢ R true true
 -/
 #guard_msgs in
 example : R true true   := by with_reducible apply_rfl -- Error
@@ -125,14 +128,16 @@ example : True' ↔ True   := by apply_rfl
 example : P true' true   := by apply_rfl
 example : Q true' true   := by apply_rfl
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   Q'
+⊢ Q' true' true'
 -/
 #guard_msgs in
 example : Q' true' true  := by apply_rfl -- Error
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   R
+⊢ R true' true'
 -/
 #guard_msgs in
 example : R true' true   := by apply_rfl -- Error
@@ -143,14 +148,16 @@ example : True' ↔ True   := by with_reducible apply_rfl
 example : P true' true   := by with_reducible apply_rfl
 example : Q true' true   := by with_reducible apply_rfl -- NB: No error, Q and true' reducible
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   Q'
+⊢ Q' true' true'
 -/
 #guard_msgs in
 example : Q' true' true  := by with_reducible apply_rfl -- Error
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   R
+⊢ R true' true'
 -/
 #guard_msgs in
 example : R true' true   := by with_reducible apply_rfl -- Error
@@ -166,22 +173,24 @@ example : True'' ↔ True   := by apply_rfl
 example : P true'' true   := by apply_rfl
 example : Q true'' true   := by apply_rfl
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   Q'
+⊢ Q' true'' true''
 -/
 #guard_msgs in
 example : Q' true'' true  := by apply_rfl -- Error
 /--
-error: rfl failed, no @[refl] lemma registered for relation
+error: tactic 'rfl' failed, no @[refl] lemma registered for relation
   R
+⊢ R true'' true''
 -/
 #guard_msgs in
 example : R true'' true   := by apply_rfl -- Error
 
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true''
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ true'' = true
 -/
@@ -197,45 +206,45 @@ with
 #guard_msgs in
 example : HEq true'' true := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   True''
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   True
 ⊢ True'' ↔ True
 -/
 #guard_msgs in
 example : True'' ↔ True   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true''
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ P true'' true
 -/
 #guard_msgs in
 example : P true'' true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true''
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ Q true'' true
 -/
 #guard_msgs in
 example : Q true'' true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true''
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ Q' true'' true
 -/
 #guard_msgs in
 example : Q' true'' true  := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true''
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ R true'' true
 -/
@@ -244,9 +253,9 @@ example : R true'' true   := by with_reducible apply_rfl -- Error
 
 -- Unequal
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ false = true
 -/
@@ -262,45 +271,45 @@ with
 #guard_msgs in
 example : HEq false true := by apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   False
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   True
 ⊢ False ↔ True
 -/
 #guard_msgs in
 example : False ↔ True   := by apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ P false true
 -/
 #guard_msgs in
 example : P false true   := by apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ Q false true
 -/
 #guard_msgs in
 example : Q false true   := by apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ Q' false true
 -/
 #guard_msgs in
 example : Q' false true  := by apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ R false true
 -/
@@ -308,9 +317,9 @@ is not definitionally equal to rhs
 example : R false true   := by apply_rfl -- Error
 
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ false = true
 -/
@@ -326,45 +335,45 @@ with
 #guard_msgs in
 example : HEq false true := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   False
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   True
 ⊢ False ↔ True
 -/
 #guard_msgs in
 example : False ↔ True   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ P false true
 -/
 #guard_msgs in
 example : P false true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ Q false true
 -/
 #guard_msgs in
 example : Q false true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ Q' false true
 -/
 #guard_msgs in
 example : Q' false true  := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   false
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   true
 ⊢ R false true
 -/
@@ -398,18 +407,18 @@ example : HEq true 1 := by with_reducible apply_rfl -- Error
 inductive S : Bool → Bool → Prop where | refl : a = true → S a a
 attribute [refl] S.refl
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   false
 ⊢ S true false
 -/
 #guard_msgs in
 example : S true false  := by apply_rfl -- Error
 /--
-error: tactic 'apply_rfl' failed, The lhs
+error: tactic 'rfl' failed, the left-hand side
   true
-is not definitionally equal to rhs
+is not definitionally equal to the right-hand side
   false
 ⊢ S true false
 -/

tests/lean/run/wfirred.lean

@@ -31,11 +31,10 @@ example : foo (n+1) = foo n := rfl
 
 -- also for closed terms
 /--
-error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+error: tactic 'rfl' failed, the left-hand side
+  foo 0
+is not definitionally equal to the right-hand side
+  0
 ⊢ foo 0 = 0
 -/
 #guard_msgs in
@@ -43,11 +42,10 @@ example : foo 0 = 0 := by rfl
 
 -- It only works on closed terms:
 /--
-error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+error: tactic 'rfl' failed, the left-hand side
+  foo (n + 1)
+is not definitionally equal to the right-hand side
+  foo n
 n : Nat
 ⊢ foo (n + 1) = foo n
 -/

tests/lean/runTacticMustCatchExceptions.lean.expected.out

@@ -1,45 +1,39 @@
-runTacticMustCatchExceptions.lean:2:25-2:28: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+runTacticMustCatchExceptions.lean:2:25-2:28: error: tactic 'rfl' failed, the left-hand side
+  1
+is not definitionally equal to the right-hand side
+  a + b
 a b : Nat
 ⊢ 1 ≤ a + b
-runTacticMustCatchExceptions.lean:3:25-3:28: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+runTacticMustCatchExceptions.lean:3:25-3:28: error: tactic 'rfl' failed, the left-hand side
+  a + b
+is not definitionally equal to the right-hand side
+  b
 a b : Nat
 this : 1 ≤ a + b
 ⊢ a + b ≤ b
-runTacticMustCatchExceptions.lean:4:25-4:28: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+runTacticMustCatchExceptions.lean:4:25-4:28: error: tactic 'rfl' failed, the left-hand side
+  b
+is not definitionally equal to the right-hand side
+  2
 a b : Nat
 this✝ : 1 ≤ a + b
 this : a + b ≤ b
 ⊢ b ≤ 2
-runTacticMustCatchExceptions.lean:9:18-9:21: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+runTacticMustCatchExceptions.lean:9:18-9:21: error: tactic 'rfl' failed, the left-hand side
+  1
+is not definitionally equal to the right-hand side
+  a + b
 a b : Nat
 ⊢ 1 ≤ a + b
-runTacticMustCatchExceptions.lean:10:14-10:17: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+runTacticMustCatchExceptions.lean:10:14-10:17: error: tactic 'rfl' failed, the left-hand side
+  a + b
+is not definitionally equal to the right-hand side
+  b
 a b : Nat
 ⊢ a + b ≤ b
-runTacticMustCatchExceptions.lean:11:14-11:17: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+runTacticMustCatchExceptions.lean:11:14-11:17: error: tactic 'rfl' failed, the left-hand side
+  b
+is not definitionally equal to the right-hand side
+  2
 a b : Nat
 ⊢ b ≤ 2