rerevert

This reverts commit e551a366a0.

src/Init/Control/Lawful/Basic.lean

@@ -33,10 +33,6 @@ 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:
@@ -87,16 +83,12 @@ 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 bind_pure_comp
+attribute [simp] pure_bind bind_assoc
 
 @[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]
 
@@ -117,21 +109,10 @@ 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 only [map_eq_pure_bind, const, seq_eq_bind_map, bind_assoc, pure_bind, id_eq, bind_pure]
+  simp [map_eq_pure_bind, seq_eq_bind_map, const]
 
 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 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]
+  rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
 
 /--
 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]
+  simp[ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont, map_eq_pure_bind]
 
 @[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, ←bind_pure_comp]
+  simp [Functor.map, ExceptT.map, map_eq_pure_bind]
   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 [←bind_pure_comp]; apply bind_congr; intro b;
+    simp [map_eq_pure_bind]; 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, ←bind_pure_comp]
+  simp [Functor.map, StateT.map, run, map_eq_pure_bind]
 
 @[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 [←bind_pure_comp, const]
+  simp [map_eq_pure_bind, 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 [←bind_pure_comp]
+  simp [map_eq_pure_bind]
 
 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
+  bind_pure_comp := by intros; apply ext; intros; simp; apply LawfulMonad.bind_pure_comp
   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,7 +823,6 @@ 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
@@ -838,9 +837,6 @@ 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

src/Init/Data/Array/Lemmas.lean

@@ -23,33 +23,11 @@ namespace Array
 
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
-theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
+theorem getElem_eq_toList_getElem (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_getElem_toList
+abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
 
 @[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
@@ -58,11 +36,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_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
+  simp only [push, getElem_eq_toList_getElem, 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_getElem_toList, List.concat_eq_append]
-  rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
+  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]
 
 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
@@ -79,7 +57,9 @@ open Array
 
 /-! ### Lemmas about `List.toArray`. -/
 
-@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
+@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
@@ -87,7 +67,6 @@ open Array
 
 @[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) := rfl
 
@@ -96,23 +75,6 @@ abbrev toArray_data := @toArray_toList
   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
@@ -259,11 +221,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_getElem_toList, ←eq]
+  simp [set, getElem_eq_toList_getElem, ←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_getElem_toList, List.getElem_set_ne h]
+  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
 
 theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
@@ -353,7 +315,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_getElem_toList]
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_toList_getElem]
 
 /-- # mem -/
 
@@ -394,7 +356,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_getElem_toList]
+  erw [Array.mem_def, getElem_eq_toList_getElem]
   apply List.get_mem
 
 theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
@@ -405,11 +367,14 @@ 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_getElem_toList, List.getElem_mem]
+  simp only [getElem_eq_toList_getElem, List.getElem_mem]
 
 @[deprecated getElem_mem_toList (since := "2024-09-09")]
 abbrev getElem_mem_data := @getElem_mem_toList
@@ -469,7 +434,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_getElem_toList, List.getElem_set_self]
+  simp only [set, getElem_eq_toList_getElem, 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]
@@ -488,7 +453,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_getElem_toList, List.getElem_set_ne h]
+  simp only [set, getElem_eq_toList_getElem, 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
@@ -517,7 +482,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]
+-- @[simp] -- FIXME: gives a weird linter error
 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]
 
@@ -590,7 +555,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_getElem_toList]
+  simp [getElem_eq_toList_getElem]
 
 set_option linter.deprecated false in
 @[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
@@ -636,32 +601,6 @@ 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
@@ -706,7 +645,7 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
-  | cons a l ih => simp [ih]
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
@@ -915,7 +854,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_getElem_toList]
+  simp only [getElem_eq_toList_getElem]
   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]
@@ -923,7 +862,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_getElem_toList]
+  simp only [getElem_eq_toList_getElem]
   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]
@@ -1136,10 +1075,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_getElem_toList]
+    rw [← getElem_eq_toList_getElem]
     exact w ⟨r, h⟩
   · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
+    exact w as[i] ⟨i, i.2, (getElem_eq_toList_getElem as 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]

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_getElem_toList, uset, toList_set] using
+  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
     List.exists_of_set _
 
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -11,7 +11,6 @@ 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
 
@@ -272,10 +271,6 @@ 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
@@ -932,10 +927,6 @@ 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
@@ -944,11 +935,6 @@ 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
@@ -1082,16 +1068,6 @@ 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
@@ -1434,10 +1410,6 @@ 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
@@ -1683,10 +1655,6 @@ 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
@@ -1776,21 +1744,6 @@ 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
@@ -2213,20 +2166,6 @@ 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 -/
 
 /--
@@ -2319,28 +2258,10 @@ 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
@@ -2348,22 +2269,6 @@ 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,7 +5,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 -/
 prelude
 import Init.Data.Int.Lemmas
-import Init.Data.Nat.Lemmas
 
 namespace Int
 
@@ -36,24 +35,10 @@ 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/Attach.lean

@@ -548,12 +548,4 @@ theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H :
     (l.attachWith p H).count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
 
-@[simp] theorem map_attach_comp_subtype_val {l : List α} :
-    l.attach.map (f ∘ Subtype.val) = l.map f := by
-  simp [map_attach]
-
-@[simp] theorem map_attachWith_comp_subtype_val {l : List α} {P : α → Prop} {H} :
-    (l.attachWith P H).map (f ∘ Subtype.val) = l.map f := by
-  simp [map_attachWith]
-
 end List

src/Init/Data/List/Lemmas.lean

@@ -1654,11 +1654,6 @@ 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'
@@ -2397,12 +2392,6 @@ 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/Nat/Lemmas.lean

@@ -767,11 +767,6 @@ 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/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,9 +2570,7 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  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
+  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
   list.
   -/
   mk ::

src/Init/Tactics.lean

@@ -149,27 +149,26 @@ 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
 
@@ -364,24 +363,31 @@ syntax (name := fail) "fail" (ppSpace str)? : tactic
 syntax (name := eqRefl) "eq_refl" : tactic
 
 /--
-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].
+`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`).
 -/
-syntax "rfl" : tactic
+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)
 
 /--
-The same as `rfl`, but without trying `eq_refl` at the end.
+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].
 -/
 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/Elab/Tactic/Rfl.lean

@@ -16,10 +16,6 @@ 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, Joachim Breitner
+Authors: Newell Jensen, Thomas Murrills
 -/
 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
-    throwTacticEx `rfl goal "expected goal to be a binary relation"
+    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
 
   -- 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
-      throwTacticEx `rfl goal <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+      throwError 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 left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
-    throwTacticEx `rfl goal explanation
+      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+    throwTacticEx `apply_rfl goal explanation
 
   if rel.isAppOfArity `Eq 1 then
     -- The common case is equality: just use `Eq.refl`
@@ -86,9 +86,6 @@ 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
@@ -105,7 +102,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
       sErr.restore
       throw e
     else
-      throwTacticEx `rfl goal m!"no @[refl] lemma registered for relation{indentExpr rel}"
+      throwError "rfl failed, 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/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -14,4 +14,3 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array
-import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Subtype

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Subtype.lean

@@ -1,57 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Lean.Meta.LitValues
-import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
-
-namespace Subtype
-open Lean Meta Simp
-
-/--
-Rewrite a function `f : { x // p x } → α` in the form `f' ∘ Subtype.val` if (syntactically) possible.
--/
-def asCompVal (f : Expr) : MetaM (Option Expr) := do
-  let Expr.lam n d b bi := f | return none
-  let_expr Subtype α p := d | return none
-  let some b' := replaceValBVar 0 b | return none
-  let f' := .lam n α b' bi
-  let r ← mkAppM ``Function.comp #[f', ← mkAppOptM ``Subtype.val #[α, p]]
-  return (some r)
-where
-  /--
-  Walk down `e`, replacing `Subtype.val #k` with `#k`,
-  and returning `none` if there are any `#k`s not in this position.
-  -/
-  replaceValBVar (k : Nat) (e : Expr) : Option Expr  :=
-    match e with
-    | .app (.app (.app (.const n _) _) _) (.bvar k') =>
-      if k = k'  then
-        if n = `Subtype.val then return .bvar k else none
-      else
-        return e
-    | .bvar i => if i = k then none else return e
-    | .app f x => return .app (← replaceValBVar k f) (← replaceValBVar k x)
-    | .lam n d b bi => return .lam n (← replaceValBVar k d) (← replaceValBVar (k+1) b) bi
-    | .forallE n d b bi => return .forallE n (← replaceValBVar k d) (← replaceValBVar (k+1) b) bi
-    | .letE n t v b d => return .letE n (← replaceValBVar k t) (← replaceValBVar k v) (← replaceValBVar (k+1) b) d
-    | .proj n i e => return .proj n i (← replaceValBVar k e)
-    | .mdata data e => return .mdata data (← replaceValBVar k e)
-    | .lit _
-    | .const _ _
-    | .sort _
-    | .mvar _
-    | .fvar _ => return e
-
-/--
-Simplify `l.map f`, where `l : List { x // p x }` and `f` factors as `f' ∘ Subtype.val`,
-to `l.map (f' ∘ Subtype.val)`.
- -/
-builtin_dsimproc [simp, seval] reduceMapSubtype (List.map _ _) := fun e => do
-  let_expr List.map _ _ f l ← e | return .continue
-  let some f' ← asCompVal f | return .continue
-  return .done <| (← mkAppM ``List.map #[f', l])
-
-end Subtype

src/Lean/MetavarContext.lean

@@ -17,13 +17,13 @@ assignments. It is used in the elaborator, tactic framework, unifier
 the requirements imposed by these modules.
 
 - We may invoke TC while executing `isDefEq`. We need this feature to
-  be able to solve unification problems such as:
+  WellFoundedRelationbe able to solve unification problems such as:
   ```
   f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
   ```
   where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`.
 
-  During `isDefEq` (i.e., unification), it will need to solve the constraint
+  During `isDefEq` (i.e., unification), it will need to solve the constrain
   ```
   ringAdd ?s =?= intAdd
   ```
@@ -179,7 +179,7 @@ the requirements imposed by these modules.
   an exception instead of return `false` whenever it tries to assign
   a metavariable owned by its caller. The idea is to sign to the caller that
   it cannot solve the TC problem at this point, and more information is needed.
-  That is, the caller must make progress and assign its metavariables before
+  That is, the caller must make progress an assign its metavariables before
   trying to invoke TC again.
 
   In Lean4, we are using a simpler design for the `MetavarContext`.

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_getElem_toList]
+      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem]
   · 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_getElem_toList]
+    rw [← Array.getElem_eq_toList_getElem]
     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_getElem_toList, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, 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_getElem_toList, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, 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_getElem_toList, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, 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_getElem_toList] at c'_in_f
+    · rw [← Array.getElem_eq_toList_getElem] 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_getElem_toList] at h'
-  rw [← Array.getElem_eq_getElem_toList] at c'_in_f
+  rw [← Array.getElem_eq_toList_getElem] at h'
+  rw [← Array.getElem_eq_toList_getElem] 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_getElem_toList, not_true_eq_false] at h3
+      simp only [List.get_eq_getElem, Array.getElem_eq_toList_getElem, 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_getElem_toList, li] at h3
+        Array.getElem_eq_toList_getElem, 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_getElem_toList, k2_eq_false, li] at li_eq_true
+        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, 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_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
+        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
       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_getElem_toList] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] 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_getElem_toList,
+        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_toList_getElem,
           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_getElem_toList, k1_eq_true, li] at li_eq_false
+        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, 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_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
+        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
       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_getElem_toList] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] 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_getElem_toList, derivedLits_arr_def, li] at h3
+        simp (config := { decide := true }) [Array.getElem_eq_toList_getElem, 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_getElem_toList, ← j_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← 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_getElem_toList, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, 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_getElem_toList, ← j1_eq_i]
+    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j1_eq_i]
       rw [← j1_eq_true]
       rfl
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j2_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← 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_getElem_toList, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, 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,8 +61,6 @@ 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
 
@@ -143,6 +141,11 @@ 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 = "LakeMain"
+root = "Lake.Main"
 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_output
+    uint8_t json
 ) {
     object * oilean_file_name = mk_option_none();
     if (ilean_file_name) {

tests/lean/Process.lean

@@ -19,6 +19,12 @@ 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,6 +2,7 @@
 0
 "ho!\n"
 "hu!\n"
+flush of broken pipe failed
 100001
 100000
 0

tests/lean/run/4644.lean

@@ -11,10 +11,11 @@ def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
   sorted_from_var a 0
 
 /--
-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
+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.
 ⊢ 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] seq_eq_bind_map
+attribute [simp] map_eq_pure_bind 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

@@ -1,25 +0,0 @@
-/-!
-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,10 +9,11 @@ This file tests the `rfl` tactic:
 -- First, let's see what `rfl` does:
 
 /--
-error: tactic 'rfl' failed, the left-hand side
-  false
-is not definitionally equal to the right-hand side
-  true
+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.
 ⊢ false = true
 -/
 #guard_msgs in
@@ -27,9 +28,9 @@ attribute [refl] P.refl
 -- Plain error
 
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   42
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   23
 ⊢ P 42 23
 -/
@@ -41,9 +42,9 @@ example : P 42 23 := by apply_rfl
 opaque withImplicitNat {n : Nat} : Nat
 
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   @withImplicitNat 42
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   @withImplicitNat 23
 ⊢ P withImplicitNat withImplicitNat
 -/
@@ -85,15 +86,13 @@ example : True ↔ True   := by apply_rfl
 example : P true true   := by apply_rfl
 example : Q true true   := by apply_rfl
 /--
-error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: rfl failed, no @[refl] lemma registered for relation
   Q'
-⊢ Q' true true
 -/
 #guard_msgs in example : Q' true true  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: rfl failed, no @[refl] lemma registered for relation
   R
-⊢ R true true
 -/
 #guard_msgs in example : R true true   := by apply_rfl -- Error
 
@@ -103,16 +102,14 @@ 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: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: 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: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: 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
@@ -128,16 +125,14 @@ example : True' ↔ True   := by apply_rfl
 example : P true' true   := by apply_rfl
 example : Q true' true   := by apply_rfl
 /--
-error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: rfl failed, no @[refl] lemma registered for relation
   Q'
-⊢ Q' true' true'
 -/
 #guard_msgs in
 example : Q' true' true  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: rfl failed, no @[refl] lemma registered for relation
   R
-⊢ R true' true'
 -/
 #guard_msgs in
 example : R true' true   := by apply_rfl -- Error
@@ -148,16 +143,14 @@ 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: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: 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: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: 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
@@ -173,24 +166,22 @@ example : True'' ↔ True   := by apply_rfl
 example : P true'' true   := by apply_rfl
 example : Q true'' true   := by apply_rfl
 /--
-error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: rfl failed, no @[refl] lemma registered for relation
   Q'
-⊢ Q' true'' true''
 -/
 #guard_msgs in
 example : Q' true'' true  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, no @[refl] lemma registered for relation
+error: 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 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true''
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ true'' = true
 -/
@@ -206,45 +197,45 @@ with
 #guard_msgs in
 example : HEq true'' true := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   True''
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   True
 ⊢ True'' ↔ True
 -/
 #guard_msgs in
 example : True'' ↔ True   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true''
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ P true'' true
 -/
 #guard_msgs in
 example : P true'' true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true''
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ Q true'' true
 -/
 #guard_msgs in
 example : Q true'' true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true''
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ Q' true'' true
 -/
 #guard_msgs in
 example : Q' true'' true  := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true''
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ R true'' true
 -/
@@ -253,9 +244,9 @@ example : R true'' true   := by with_reducible apply_rfl -- Error
 
 -- Unequal
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ false = true
 -/
@@ -271,45 +262,45 @@ with
 #guard_msgs in
 example : HEq false true := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   False
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   True
 ⊢ False ↔ True
 -/
 #guard_msgs in
 example : False ↔ True   := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ P false true
 -/
 #guard_msgs in
 example : P false true   := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ Q false true
 -/
 #guard_msgs in
 example : Q false true   := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ Q' false true
 -/
 #guard_msgs in
 example : Q' false true  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ R false true
 -/
@@ -317,9 +308,9 @@ is not definitionally equal to the right-hand side
 example : R false true   := by apply_rfl -- Error
 
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ false = true
 -/
@@ -335,45 +326,45 @@ with
 #guard_msgs in
 example : HEq false true := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   False
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   True
 ⊢ False ↔ True
 -/
 #guard_msgs in
 example : False ↔ True   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ P false true
 -/
 #guard_msgs in
 example : P false true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ Q false true
 -/
 #guard_msgs in
 example : Q false true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ Q' false true
 -/
 #guard_msgs in
 example : Q' false true  := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   false
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   true
 ⊢ R false true
 -/
@@ -407,18 +398,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 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   false
 ⊢ S true false
 -/
 #guard_msgs in
 example : S true false  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, the left-hand side
+error: tactic 'apply_rfl' failed, The lhs
   true
-is not definitionally equal to the right-hand side
+is not definitionally equal to rhs
   false
 ⊢ S true false
 -/

tests/lean/run/simprocSubtype.lean

@@ -1,8 +0,0 @@
-inductive Tree where | node : List Tree → Tree
-
-def Tree.rev : Tree → Tree
-  | node ts => .node (ts.attach.reverse.map (fun ⟨t, _⟩ => t.rev))
-
-@[simp] theorem Tree.rev_def (ts : List Tree) :
-    Tree.rev (.node ts) = .node (ts.reverse.map rev) := by
-  simp [Tree.rev]

tests/lean/run/wfirred.lean

@@ -31,10 +31,11 @@ example : foo (n+1) = foo n := rfl
 
 -- also for closed terms
 /--
-error: tactic 'rfl' failed, the left-hand side
-  foo 0
-is not definitionally equal to the right-hand side
-  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.
 ⊢ foo 0 = 0
 -/
 #guard_msgs in
@@ -42,10 +43,11 @@ example : foo 0 = 0 := by rfl
 
 -- It only works on closed terms:
 /--
-error: tactic 'rfl' failed, the left-hand side
-  foo (n + 1)
-is not definitionally equal to the right-hand side
-  foo n
+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.
 n : Nat
 ⊢ foo (n + 1) = foo n
 -/

tests/lean/runTacticMustCatchExceptions.lean.expected.out

@@ -1,39 +1,45 @@
-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
+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.
 a b : Nat
 ⊢ 1 ≤ a + b
-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
+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.
 a b : Nat
 this : 1 ≤ a + b
 ⊢ a + b ≤ b
-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
+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.
 a b : Nat
 this✝ : 1 ≤ a + b
 this : a + b ≤ b
 ⊢ b ≤ 2
-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
+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.
 a b : Nat
 ⊢ 1 ≤ a + b
-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
+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.
 a b : Nat
 ⊢ a + b ≤ b
-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
+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.
 a b : Nat
 ⊢ b ≤ 2