chore: reordering in Array.Basic

doc/dev/release_checklist.md

@@ -71,12 +71,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

src/Init/Core.lean

@@ -1382,11 +1382,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

@@ -162,16 +162,19 @@ instance : Inhabited (Array α) where
 @[simp] def isEmpty (a : Array α) : Bool :=
   a.size = 0
 
+-- TODO(Leo): cleanup
 @[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) :
-    ∀ (i : Nat) (_ : i ≤ a.size), Bool
-  | 0, _ => true
-  | i+1, h =>
-    p a[i] (b[i]'(hsz ▸ h)) && isEqvAux a b hsz p i (Nat.le_trans (Nat.le_add_right i 1) h)
+def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
+  if h : i < a.size then
+     have : i < b.size := hsz ▸ h
+     p a[i] b[i] && isEqvAux a b hsz p (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
-    isEqvAux a b h p a.size (Nat.le_refl a.size)
+    isEqvAux a b h p 0
   else
     false
 
@@ -185,10 +188,9 @@ ofFn f = #[f 0, f 1, ... , f(n - 1)]
 ``` -/
 def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-  decreasing_by simp_wf; decreasing_trivial_pre_omega
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -387,12 +389,11 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    map (i : Nat) (r : Array β) : m (Array β) := do
-      if hlt : i < as.size then
-        map (i+1) (r.push (← f as[i]))
-      else
-        pure r
+  let rec map (i : Nat) (r : Array β) : m (Array β) := do
+    if hlt : i < as.size then
+      map (i+1) (r.push (← f as[i]))
+    else
+      pure r
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -456,8 +457,7 @@ unsafe def anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α →
 @[implemented_by anyMUnsafe]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    loop (j : Nat) : m Bool := do
+    let rec loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -547,8 +547,7 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -558,7 +557,6 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
   a.findIdx? fun a => a == v
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
     let idx : Fin a.size := ⟨i, h⟩;
@@ -680,7 +678,6 @@ where
     else
       as
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
@@ -692,8 +689,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  go (i : Nat) (r : Array α) : Array α :=
+  let rec go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
       let a := as.get ⟨i, h⟩
       if p a then
@@ -709,7 +705,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   if h : i.val + 1 < a.size then
     let a' := a.swap ⟨i.val + 1, h⟩ i
@@ -744,8 +739,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
 
 /-- Insert element `a` at position `i`. -/
 @[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (as : Array α) (j : Fin as.size) :=
+  let rec loop (as : Array α) (j : Fin as.size) :=
     if i.1 < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -763,7 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -785,8 +778,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
-def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
+@[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
     if h : i < bs.size then
@@ -822,7 +814,6 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
-@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   if h : i < as.size then
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)

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

src/Init/Data/Array/DecidableEq.lean

@@ -9,37 +9,37 @@ import Init.ByCases
 
 namespace Array
 
-theorem eq_of_isEqvAux
-    [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
-    (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i hi)
-    (j : Nat) (hj : j < i) : a[j]'(Nat.lt_of_lt_of_le hj hi) = b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)) := by
-  induction i with
-  | zero => contradiction
-  | succ i ih =>
-    simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv
-    by_cases hj' : j < i
-    next =>
-      exact ih _ heqv.right hj'
-    next =>
-      replace hj' : j = i := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp hj') hj
-      subst hj'
-      exact heqv.left
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a[j] = b[j]'(hsz ▸ high) := by
+  by_cases h : i < a.size
+  · unfold Array.isEqvAux at heqv
+    simp [h] at heqv
+    have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
+    by_cases heq : i = j
+    · subst heq; exact heqv.1
+    · exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne low heq)) high
+  · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
+    subst heq
+    exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
+termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
+
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
   split
   next hsz =>
    intro h
-   have aux := eq_of_isEqvAux a b hsz a.size (Nat.le_refl ..) h
-   exact ext a b hsz fun i h _ => aux i h
+   have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
+   exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
   next => intro; contradiction
 
-theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) (h : i ≤ a.size) :
-    Array.isEqvAux a a rfl (fun x y => x = y) i h = true := by
-  induction i with
-  | zero => simp [Array.isEqvAux]
-  | succ i ih =>
-    simp_all only [isEqvAux, decide_True, Bool.and_self]
+theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by
+  unfold Array.isEqvAux
+  split
+  next h => simp [h, isEqvAux_self a (i+1)]
+  next h => simp [h]
+termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -19,14 +19,24 @@ 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
+attribute [simp] uset
 
-@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
-@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
+@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
+  | ⟨l⟩ => ext' (toList_toArray l)
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+
+@[deprecated toList_length (since := "2024-09-09")]
+abbrev data_length := @toList_length
+
+@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
+
+@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
 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
@@ -36,7 +46,27 @@ 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
-  simp
+  simp [getElem_eq_toList_getElem]
+
+theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
+  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
+
+@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
+  simp [← foldrM_push]
+
+theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
+
+@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
+
+/-- A more efficient version of `arr.toList.reverse`. -/
+@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
+
+@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
+  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 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]
@@ -54,78 +84,6 @@ theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
   · simp at h
     simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
-end Array
-
-namespace List
-
-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 α} :
-    (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 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₂
-
-@[simp] theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
-end List
-
-namespace Array
-
-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 toList_length {l : Array α} : l.toList.length = l.size := rfl
-
-@[deprecated toList_length (since := "2024-09-09")]
-abbrev data_length := @toList_length
-
-@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
-
-@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
-
-theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
-
-/-- Variant of `foldrM_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
-@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
-  simp [← foldrM_push]
-
-theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
-
-/-- Variant of `foldr_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
-@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
-    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
-
-/-- A more efficient version of `arr.toList.reverse`. -/
-@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
-
-@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
-
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
   rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
@@ -387,7 +345,7 @@ theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList :
 abbrev getElem_mem_data := @getElem_mem_toList
 
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
 
 @[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
@@ -647,12 +605,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]
+  | nil => simp; rfl
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList

src/Init/Data/Array/TakeDrop.lean

@@ -12,7 +12,6 @@ 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
-    List.exists_of_set _
+  simpa [Array.getElem_eq_toList_getElem] using List.exists_of_set _
 
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -710,26 +710,6 @@ theorem or_comm (x y : BitVec w) :
   simp [Bool.or_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩
 
-@[simp] theorem or_self {x : BitVec w} : x ||| x = x := by
-  ext i
-  simp
-
-@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
-  ext i
-  simp
-
-@[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
-  ext i
-  simp
-
-@[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i
-  simp
-
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -771,26 +751,6 @@ theorem and_comm (x y : BitVec w) :
   simp [Bool.and_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩
 
-@[simp] theorem and_self {x : BitVec w} : x &&& x = x := by
-  ext i
-  simp
-
-@[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i
-  simp
-
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -835,18 +795,6 @@ theorem xor_comm (x y : BitVec w) :
   simp [Bool.xor_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩
 
-@[simp] theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by
-  ext i
-  simp
-
-@[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
-  ext i
-  simp
-
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -895,14 +843,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
-@[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i
-  simp
-
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by

src/Init/Data/List/Lemmas.lean

@@ -938,38 +938,6 @@ def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β →
         x (mem_cons_self x l) :=
   rfl
 
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
-    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldl_cons]
-    apply ih
-    · simp_all
-    · exact fun a m c c' h => h' _ (by simp_all) _ _ h
-
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
-    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldr_cons]
-    apply h'
-    · simp
-    · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
-
 /-! ### getLast -/
 
 theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
@@ -1314,16 +1282,11 @@ theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by
 theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs => f a :: bs) [] l := by
   induction l <;> simp [*]
 
-@[simp] theorem map_set {f : α → β} {l : List α} {i : Nat} {a : α} :
-    (l.set i a).map f = (l.map f).set i (f a) := by
-  induction l generalizing i with
-  | nil => simp
-  | cons b l ih => cases i <;> simp_all
-
-@[deprecated "Use the reverse direction of `map_set`." (since := "2024-09-20")]
-theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
+@[simp] theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
     (map f l).set n (f a) = map f (l.set n a) := by
-  simp
+  induction l generalizing n with
+  | nil => simp
+  | cons b l ih => cases n <;> simp_all
 
 @[simp] theorem head_map (f : α → β) (l : List α) (w) :
     head (map f l) w = f (head l (by simpa using w)) := by

src/Init/Data/Repr.lean

@@ -51,12 +51,6 @@ instance [Repr α] : Repr (id α) :=
 instance [Repr α] : Repr (Id α) :=
   inferInstanceAs (Repr α)
 
-/-
-This instance allows us to use `Empty` as a type parameter without causing instance synthesis to fail.
--/
-instance : Repr Empty where
-  reprPrec := nofun
-
 instance : Repr Bool where
   reprPrec
     | true, _  => "true"
@@ -163,7 +157,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

@@ -2709,10 +2709,7 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
--/
+/-- Auxiliary definition for `List.toArray`. -/
 @[inline_if_reduce]
 def List.toArrayAux : List α → Array α → Array α
   | nil,       r => r

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/PatternVar.lean

@@ -156,11 +156,9 @@ private def processVar (idStx : Syntax) : M Syntax := do
   modify fun s => { s with vars := s.vars.push idStx, found := s.found.insert id }
   return idStx
 
-private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do
-  if h₁ : s₁.vars.size = s₂.vars.size then
-    for h₂ : i in [startingAt:s₁.vars.size] do
-      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false
-    true
+private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool :=
+  if h : s₁.vars.size = s₂.vars.size then
+    Array.isEqvAux s₁.vars s₂.vars h (.==.) startingAt
   else
     false
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -35,7 +35,7 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
 expression - pair values.
 -/
 def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
-    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat Expr) :
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
   for (bitVar, cnfVar) in var2Cnf.toArray do
@@ -70,7 +70,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
+    let atomExpr := atomsAssignment.get! bitVecVar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -83,14 +83,14 @@ structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) → MetaM UnsatProver.Result
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result
 
 /--
 Contains values that will be used to diagnose spurious counter examples.
 -/
 structure DiagnosisInput where
   unusedHypotheses : Std.HashSet FVarId
-  atomsAssignment : Std.HashMap Nat (Nat × Expr)
+  atomsAssignment : Std.HashMap Nat Expr
 
 /--
 The result of a spurious counter example diagnosis.
@@ -104,14 +104,14 @@ abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnos
 namespace DiagnosisM
 
 def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM Diagnosis := do
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
   let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
   return issues
 
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
 
-def atomsAssignment : DiagnosisM (Std.HashMap Nat (Nat × Expr)) := do
+def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
   return (← read).atomsAssignment
 
 def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
@@ -131,7 +131,7 @@ Diagnose spurious counter examples, currently this checks:
 - Whether all hypotheses which contain any variable that was bitblasted were included
 -/
 def diagnose : DiagnosisM Unit := do
-  for (_, (_, expr)) in ← atomsAssignment do
+  for (_, expr) in ← atomsAssignment do
     match_expr expr with
     | BitVec.ofBool x =>
       match x with
@@ -158,7 +158,7 @@ def explainers : List (Diagnosis → Option MessageData) :=
   [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
 
 def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM MessageData := do
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
   let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
   let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
   let explanations := explainers.foldl (init := #[]) folder
@@ -172,7 +172,7 @@ def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
     return err
 
 def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (atomsAssignment : Std.HashMap Nat Expr) :
     MetaM UnsatProver.Result := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
@@ -242,7 +242,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
         reflectBV g
     trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
-    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
+    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
     let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
     let proveFalse ← reflectionResult.proveFalse bvExprUnsat

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -141,11 +141,10 @@ This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwis
 def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
     (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool)
     : MetaM (Except (Array (Bool × Nat)) LratCert) := do
-  IO.FS.withTempFile fun cnfHandle cnfPath => do
+  IO.FS.withTempFile fun _ cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
       -- lazyPure to prevent compiler lifting
-      cnfHandle.putStr  (← IO.lazyPure (fun _ => cnf.dimacs))
-      cnfHandle.flush
+      IO.FS.writeFile cnfPath (← IO.lazyPure (fun _ => cnf.dimacs))
 
     let res ←
       withTraceNode `sat (fun _ => return "Running SAT solver") do

src/Lean/Elab/Tactic/Basic.lean

@@ -49,9 +49,6 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
-instance : Inhabited (TacticM α) where
-  default := fun _ _ => default
-
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 

src/Lean/Meta/Instances.lean

@@ -113,34 +113,8 @@ For example:
     (because A B are out-params and are only filled in once we synthesize 2)
 
 (The type of `inst` must not contain mvars.)
-
-Remark: `projInfo?` is `some` if the instance is a projection.
-We need this information because of the heuristic we use to annotate binder
-information in projections. See PR #5376 and issue #5333. Before PR
-#5376, given a class `C` at
-```
-class A (n : Nat) where
-
-instance [A n] : A n.succ where
-
-class B [A 20050] where
-
-class C [A 20000] extends B where
-```
-we would get the following instance
-```
-C.toB [inst : A 20000] [self : @C inst] : @B ...
-```
-After the PR, we have
-```
-C.toB {inst : A 20000} [self : @C inst] : @B ...
-```
-Note the attribute `inst` is now just a regular implicit argument.
-To ensure `computeSynthOrder` works as expected, we should take
-this change into account while processing field `self`.
-This field is the one at position `projInfo?.numParams`.
 -/
-private partial def computeSynthOrder (inst : Expr) (projInfo? : Option ProjectionFunctionInfo) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -177,8 +151,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   let tyOutParams ← getSemiOutParamPositionsOf ty
   let tyArgs := ty.getAppArgs
   for tyArg in tyArgs, i in [:tyArgs.size] do
-    unless tyOutParams.contains i do
-      assignMVarsIn tyArg
+    unless tyOutParams.contains i do assignMVarsIn tyArg
 
   -- Now we successively try to find the next ready subgoal, where all
   -- non-out-params are mvar-free.
@@ -186,13 +159,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray
   while !toSynth.isEmpty do
     let next? ← toSynth.findM? fun i => do
-      let argTy ← instantiateMVars (← inferType argMVars[i]!)
-      if let some projInfo := projInfo? then
-        if projInfo.numParams == i then
-          -- See comment regarding `projInfo?` at the beginning of this function
-          assignMVarsIn argTy
-          return true
-      forallTelescopeReducing argTy fun _ argTy => do
+      forallTelescopeReducing (← instantiateMVars (← inferType argMVars[i]!)) fun _ argTy => do
       let argTy ← whnf argTy
       let argOutParams ← getSemiOutParamPositionsOf argTy
       let argTyArgs := argTy.getAppArgs
@@ -228,8 +195,7 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let projInfo? ← getProjectionFnInfo? declName
-  let synthOrder ← computeSynthOrder c projInfo?
+  let synthOrder ← computeSynthOrder c
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize

src/Lean/Meta/Tactic/Refl.lean

@@ -12,9 +12,6 @@ namespace Lean.Meta
 
 /--
 Close given goal using `Eq.refl`.
-
-See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
-backs the `rfl` tactic.
 -/
 def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do

src/Lean/Meta/Tactic/Rfl.lean

@@ -50,59 +50,33 @@ open Elab Tactic
 
 /-- `MetaM` version of the `rfl` tactic.
 
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, equality or another relation which has a reflexive lemma tagged with the
-attribute [refl].
+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].
 -/
-def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
-  -- 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)}"
-
-  -- 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{
-        goalsToMessageData gs}"
-    return
-
-  let rel := t.appFn!.appFn!
-  let lhs := t.appFn!.appArg!
-  let rhs := t.appArg!
-
-  let success ← approxDefEq <| isDefEqGuarded lhs rhs
-  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
-
-  if rel.isAppOfArity `Eq 1 then
-    -- The common case is equality: just use `Eq.refl`
-    let us := rel.appFn!.constLevels!
-    let α :=  rel.appArg!
-    goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
+  let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
+    | throwError "reflexivity lemmas only apply to binary relations, not{
+        indentExpr (← goal.getType)}"
+  if let .app (.const ``Eq [_]) _ := rel then
+    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
   else
-    -- Else search through `@refl` keyed by the relation
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
       try
         let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
         if gs.isEmpty then return () else
-          throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+          logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        unless ex?.isSome do
-          ex? := some (← saveState, e) -- stash the first failure of `apply`
+        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
       s.restore
     if let some (sErr, e) := ex? then
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
+      throwError "rfl failed, no lemma with @[refl] applies"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

src/Lean/ProjFns.lean

@@ -21,7 +21,7 @@ structure ProjectionFunctionInfo where
   i : Nat
   /-- `true` if the structure is a class. -/
   fromClass : Bool
-  deriving Inhabited, Repr
+  deriving Inhabited
 
 @[export lean_mk_projection_info]
 def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=

src/Std/Data/DHashMap/Basic.lean

@@ -186,15 +186,6 @@ section Unverified
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : (a : α) → β a → Bool)
-    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
-  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
-    if f a b then
-      (l.insert a b, r)
-    else
-      (l, r.insert a b)
-
 @[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
@@ -269,10 +260,6 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
-@[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
-    DHashMap α (fun _ => Unit) :=
-  Const.insertManyUnit ∅ l
-
 @[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1

src/Std/Data/DHashMap/Raw.lean

@@ -411,14 +411,6 @@ This is mainly useful to implement `HashSet.ofList`, so if you are considering u
     Raw α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
-/-- Creates a hash map from an array of keys, associating the value `()` with each key.
-
-This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
-`HashSet` or `HashSet.Raw` might be a better fit for you. -/
-@[inline] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
-    Raw α (fun _ => Unit) :=
-  Const.insertManyUnit ∅ l
-
 /--
 Returns the number of buckets in the internal representation of the hash map. This function may be
 useful for things like monitoring system health, but it should be considered an internal

src/Std/Data/HashMap/Basic.lean

@@ -190,11 +190,6 @@ section Unverified
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
-@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
-    (m : HashMap α β) : HashMap α β × HashMap α β :=
-  let ⟨l, r⟩ := m.inner.partition f
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 @[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
@@ -255,10 +250,6 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
-@[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
-    HashMap α Unit :=
-  ⟨DHashMap.Const.unitOfArray l⟩
-
 @[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner

src/Std/Data/HashSet/Basic.lean

@@ -158,11 +158,6 @@ section Unverified
 @[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
-  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
@@ -217,14 +212,6 @@ in the collection will be present in the returned hash set.
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
   ⟨HashMap.unitOfList l⟩
 
-/--
-Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
-collection contains multiple elements that are equal (with regard to `==`), then the last element
-in the collection will be present in the returned hash set.
--/
-@[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : HashSet α :=
-  ⟨HashMap.unitOfArray l⟩
-
 /-- Computes the union of the given hash sets. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α :=
   m₂.fold (init := m₁) fun acc x => acc.insert x

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -142,8 +142,8 @@ def toString : BVUnOp → String
   | not => "~"
   | shiftLeftConst n => s!"<< {n}"
   | shiftRightConst n => s!">> {n}"
-  | rotateLeft n => s!"rotL {n}"
-  | rotateRight n => s!"rotR {n}"
+  | rotateLeft n => s! "rotL {n}"
+  | rotateRight n => s! "rotR {n}"
   | arithShiftRightConst n => s!">>a {n}"
 
 instance : ToString BVUnOp := ⟨toString⟩
@@ -238,7 +238,7 @@ def toString : BVExpr w → String
   | .var idx => s!"var{idx}"
   | .const val => ToString.toString val
   | .zeroExtend v expr => s!"(zext {v} {expr.toString})"
-  | .extract start len expr => s!"{expr.toString}[{start}, {len}]"
+  | .extract hi lo expr => s!"{expr.toString}[{hi}:{lo}]"
   | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
   | .un op operand => s!"({op.toString} {toString operand})"
   | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})"

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

@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [Array.foldr_eq_foldr_toList, List.toArray_toList] at h2
+    rw [Array.foldr_eq_foldr_toList, Array.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+              rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+            rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))

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

@@ -500,7 +500,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
+                conv => rhs; rw [f_clauses_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
@@ -533,7 +534,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
+                conv => rhs; rw [f_clauses_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
@@ -593,7 +595,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                conv => rhs; rw [Array.size_mk]
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
+                conv => rhs; rw [f_clauses_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

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

@@ -1112,7 +1112,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
     (derivedLits : CNF.Clause (PosFin n))
     (derivedLits_satisfies_invariant:
       DerivedLitsInvariant f f_assignments_size (performRupCheck f rupHints).fst.assignments f'_assignments_size derivedLits)
-    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits })
+    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def: derivedLits_arr = { toList := derivedLits })
     (i j : Fin (Array.size derivedLits_arr)) (i_ne_j : i ≠ j) :
     derivedLits_arr[i] ≠ derivedLits_arr[j] := by
   intro li_eq_lj

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

@@ -543,8 +543,8 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
 theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) :
     (reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
-  let c_arr := c.clause.toArray
-  have c_clause_rw : c.clause = c_arr.toList := by simp [c_arr]
+  let c_arr := Array.mk c.clause
+  have c_clause_rw : c.clause = c_arr.toList := rfl
   rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by

src/library/constructions/projection.cpp

@@ -63,8 +63,6 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             // 1. The original binder before `mk_outparam_args_implicit` is not an instance implicit.
             // 2. It is not originally an outparam. Outparams must be implicit.
             bi = mk_binder_info();
-        } else if (is_inst_implicit(bi_orig) && inst_implicit) {
-            bi = mk_implicit_binder_info();
         }
         expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type), type, bi);
         cnstr_type = instantiate(binding_body(cnstr_type), param);

tests/lean/run/2670.lean

@@ -12,12 +12,12 @@ def enumFromTR' (n : Nat) (l : List α) : List (Nat × α) :=
 
 open List in
 theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
-  funext α n l; simp only [enumFromTR']
+  funext α n l; simp [enumFromTR', -Array.size_toArray]
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
     | [], n => rfl
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
+  rw [Array.foldr_eq_foldr_data]
   simp [go] -- Should close the goal

tests/lean/run/5333.lean

@@ -1,20 +0,0 @@
-class A (n : Nat) where
-
-instance [A n] : A n.succ where
-
-class B [A 20050] where
-
-set_option trace.Meta.debug true
-
-class C [A 20000] extends B where
-
-#check C.toB
-
-instance : A 20050 where
-
-class D where
-
-instance inst1 : D where
-instance inst2 [B] : D where
-
-#synth D

tests/lean/run/array_isEqvAux.lean

@@ -1,45 +0,0 @@
-
-/-!
-Because `Array.isEqvAux` was defined by well-founded recursion, this used to fail with
-```
-tactic 'decide' failed for proposition
-  #[0, 1] = #[0, 1]
-since its 'Decidable' instance
-  #[0, 1].instDecidableEq #[0, 1]
-did not reduce to 'isTrue' or 'isFalse'.
-
-After unfolding the instances 'instDecidableEqNat', 'Array.instDecidableEq' and 'Nat.decEq', reduction got stuck at the 'Decidable' instance
-  match h : #[0, 1].isEqv #[0, 1] fun a b => decide (a = b) with
-  | true => isTrue ⋯
-  | false => isFalse ⋯
-```
--/
-
-example : #[0, 1] = #[0, 1] := by decide
-
-/-!
-There are other `Array` functions that use well-founded recursion,
-which we've marked as `@[semireducible]`. We test that `decide` can unfold them here.
--/
-
-example : Array.ofFn (id : Fin 2 → Fin 2) = #[0, 1] := by decide
-
-example : #[0, 1].map (· + 1) = #[1, 2] := by decide
-
-example : #[0, 1].any (· % 2 = 0) := by decide
-
-example : #[0, 1].findIdx? (· % 2 = 0) = some 0 := by decide
-
-example : #[0, 1, 2].popWhile (· % 2 = 0) = #[0, 1] := by decide
-
-example : #[0, 1, 2].takeWhile (· % 2 = 0) = #[0] := by decide
-
-example : #[0, 1, 2].feraseIdx ⟨1, by decide⟩ = #[0, 2] := by decide
-
-example : #[0, 1, 2].insertAt ⟨1, by decide⟩ 3 = #[0, 3, 1, 2] := by decide
-
-example : #[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true := by decide
-
-example : #[0, 1, 2].zipWith #[3, 4, 5] (· + ·) = #[3, 5, 7] := by decide
-
-example : #[0, 1, 2].allDiff = true := by decide

tests/lean/run/overAndPartialAppsAtWF.lean

@@ -1,17 +1,7 @@
-@[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
-  if h : i < a.size then
-     have : i < b.size := hsz ▸ h
-     p a[i] b[i] && isEqvAux a b hsz p (i+1)
-  else
-    true
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
   intro j low high
   by_cases h : i < a.size
-  · unfold isEqvAux at heqv
+  · unfold Array.isEqvAux at heqv
     simp [h] at heqv
     have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
     by_cases heq : i = j

tests/lean/run/repr_empty.lean

@@ -1,29 +0,0 @@
-/-!
-# Validation of `Repr Empty` instance
-
-While it may seem unnecessary to have Repr, it prevents the automatic derivation
-of Repr for other types when `Empty` is used as a type parameter.
-
-This is a simplified version of an example from the "Functional Programming in Lean" book.
-The Empty type is used to exlude the `other` constructor from the `Prim` type.
--/
-
-inductive Prim (special : Type) where
-  | plus
-  | minus
-  | other : special → Prim special
-deriving Repr
-
-/-!
-Check that both Repr's work
--/
-
-/-- info: Prim.plus -/
-#guard_msgs in
-open Prim in
-#eval (plus : Prim Int)
-
-/-- info: Prim.minus -/
-#guard_msgs in
-open Prim in
-#eval (minus : Prim Empty)

tests/lean/run/rflApplyFoApprox.lean

@@ -1,15 +0,0 @@
-
-opaque f : Nat → Nat
--- A rewrite with a free variable on the RHS
-
-opaque P : Nat → (Nat → Nat) → Prop
-opaque Q : Nat → Prop
-opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
-
-example : P x f ↔ Q (x + 10) := by
-  rewrite [foo]
-  -- we have an mvar now
-  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
-  -- same as
-  -- with_reducible (apply (Iff.refl _))
-  -- NB: apply, not exact! Different defEq flags.

tests/lean/run/rflTacticErrors.lean

@@ -1,445 +0,0 @@
-
-/-!
-This file tests the `rfl` tactic:
- * Extensibility
- * Error messages
- * Effect of `with_reducible`
--/
-
--- 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.
-⊢ false = true
--/
-#guard_msgs in
-example : false = true := by rfl
-
--- Now to `apply_rfl`.
-
--- A plain reflexive predicate
-inductive P : α → α → Prop where | refl : P a a
-attribute [refl] P.refl
-
--- Plain error
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  42
-is not definitionally equal to rhs
-  23
-⊢ P 42 23
--/
-#guard_msgs in
-example : P 42 23 := by apply_rfl
-
--- Revealing implicit arguments
-
-opaque withImplicitNat {n : Nat} : Nat
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  @withImplicitNat 42
-is not definitionally equal to rhs
-  @withImplicitNat 23
-⊢ P withImplicitNat withImplicitNat
--/
-#guard_msgs in
-example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
-
-
--- Exhaustive testing of various combinations:
-
--- In addition to Eq, HEq and Iff  we test four relations:
-
-
--- Defeq to relation `P` at reducible transparency
-abbrev Q : α → α → Prop := P
-
--- Defeq to relation `P` at default transparency
-def Q' : α → α → Prop := P
-
--- No refl attribute
-inductive R : α → α → Prop where | refl : R a a
-
-
-/-
-Now we systematically test all relations with
-* syntactic equal arguments
-* reducibly equal arguments
-* semireducibly equal arguments
-* nonequal arguments
-
-and all using `apply_rfl` and `with_reducible apply_rfl`
--/
-
-
--- Syntactic equal
-
-example : true = true   := by apply_rfl
-example : HEq true true := by apply_rfl
-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
-  Q'
--/
-#guard_msgs in example : Q' true true  := by apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in example : R true true   := by apply_rfl -- Error
-
-example : true = true   := by with_reducible apply_rfl
-example : HEq true true := by with_reducible apply_rfl
-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
-  Q'
--/
-#guard_msgs in
-example : Q' true true  := by with_reducible apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true true   := by with_reducible apply_rfl -- Error
-
--- Reducibly equal
-
-abbrev true' := true
-abbrev True' := True
-
-example : true' = true   := by apply_rfl
-example : HEq true' true := by apply_rfl
-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
-  Q'
--/
-#guard_msgs in
-example : Q' true' true  := by apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true' true   := by apply_rfl -- Error
-
-example : true' = true   := by with_reducible apply_rfl
-example : HEq true' true := by with_reducible apply_rfl
-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
-  Q'
--/
-#guard_msgs in
-example : Q' true' true  := by with_reducible apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true' true   := by with_reducible apply_rfl -- Error
-
--- Equal at default transparency only
-
-def true'' := true
-def True'' := True
-
-example : true'' = true   := by apply_rfl
-example : HEq true'' true := by apply_rfl
-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
-  Q'
--/
-#guard_msgs in
-example : Q' true'' true  := by apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true'' true   := by apply_rfl -- Error
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ true'' = true
--/
-#guard_msgs in
-example : true'' = true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  @HEq ?α ?a ?α ?a
-with
-  @HEq Bool true'' Bool true
-⊢ HEq true'' true
--/
-#guard_msgs in
-example : HEq true'' true := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  True''
-is not definitionally equal to rhs
-  True
-⊢ True'' ↔ True
--/
-#guard_msgs in
-example : True'' ↔ True   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-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 'apply_rfl' failed, The lhs
-  true''
-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 'apply_rfl' failed, The lhs
-  true''
-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 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ R true'' true
--/
-#guard_msgs in
-example : R true'' true   := by with_reducible apply_rfl -- Error
-
--- Unequal
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ false = true
--/
-#guard_msgs in
-example : false = true   := by apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq false true
-⊢ HEq false true
--/
-#guard_msgs in
-example : HEq false true := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  False
-is not definitionally equal to rhs
-  True
-⊢ False ↔ True
--/
-#guard_msgs in
-example : False ↔ True   := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ P false true
--/
-#guard_msgs in
-example : P false true   := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q false true
--/
-#guard_msgs in
-example : Q false true   := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q' false true
--/
-#guard_msgs in
-example : Q' false true  := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ R false true
--/
-#guard_msgs in
-example : R false true   := by apply_rfl -- Error
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ false = true
--/
-#guard_msgs in
-example : false = true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq false true
-⊢ HEq false true
--/
-#guard_msgs in
-example : HEq false true := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  False
-is not definitionally equal to rhs
-  True
-⊢ False ↔ True
--/
-#guard_msgs in
-example : False ↔ True   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-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 'apply_rfl' failed, The lhs
-  false
-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 'apply_rfl' failed, The lhs
-  false
-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 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ R false true
--/
-#guard_msgs in
-example : R false true   := by with_reducible apply_rfl -- Error
-
--- Inheterogeneous unequal
-
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq true 1
-⊢ HEq true 1
--/
-#guard_msgs in
-example : HEq true 1 := by apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq true 1
-⊢ HEq true 1
--/
-#guard_msgs in
-example : HEq true 1 := by with_reducible apply_rfl -- Error
-
--- Rfl lemma with side condition:
--- Error message should show left-over goal
-
-inductive S : Bool → Bool → Prop where | refl : a = true → S a a
-attribute [refl] S.refl
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true
-is not definitionally equal to rhs
-  false
-⊢ S true false
--/
-#guard_msgs in
-example : S true false  := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true
-is not definitionally equal to rhs
-  false
-⊢ S true false
--/
-#guard_msgs in
-example : S true false  := by with_reducible apply_rfl -- Error
-/--
-error: unsolved goals
-case a
-⊢ true = true
--/
-#guard_msgs in
-example : S true true   := by apply_rfl -- Error (left-over goal)
-/--
-error: unsolved goals
-case a
-⊢ true = true
--/
-#guard_msgs in
-example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
-/--
-error: unsolved goals
-case a
-⊢ false = true
--/
-#guard_msgs in
-example : S false false := by apply_rfl -- Error (left-over goal)
-/--
-error: unsolved goals
-case a
-⊢ false = true
--/
-#guard_msgs in
-example : S false false := by with_reducible apply_rfl -- Error (left-over goal)