fix: Float32 runtime support

This PR adds missing features and fixes bugs in the `Float32` support

CODEOWNERS

@@ -4,7 +4,7 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @kim-em
+/.github/ @Kha @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
@@ -14,7 +14,9 @@
 /src/Lean/Elab/Tactic/ @kim-em
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/PrettyPrinter/ @kmill
+/src/Lean/Parser/ @Kha
+/src/Lean/PrettyPrinter/ @Kha
+/src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/Init/Data/ @kim-em

src/Init/Data/Array/Basic.lean

@@ -663,7 +663,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any (a == ·)
+  as.any (· == a)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a

src/Init/Data/Array/Lemmas.lean

@@ -19,6 +19,8 @@ import Init.Data.List.ToArray
 ## Theorems about `Array`.
 -/
 
+
+
 namespace Array
 
 /-! ## Preliminaries -/
@@ -182,14 +184,6 @@ theorem getElem_eq_getElem?_get (a : Array α) (i : Nat) (h : i < a.size) :
     a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
-    a[i]?.getD d = if p : i < a.size then a[i]'p else d := by
-  if h : i < a.size then
-    simp [h, getElem?_def]
-  else
-    have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [getElem?_eq_none p, h]
-
 @[simp] theorem getElem?_empty {n : Nat} : (#[] : Array α)[n]? = none := rfl
 
 theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
@@ -385,22 +379,6 @@ theorem isEmpty_iff_size_eq_zero {l : Array α} : l.isEmpty ↔ l.size = 0 := by
 @[simp] theorem isEmpty_eq_false {l : Array α} : l.isEmpty = false ↔ l ≠ #[] := by
   cases l <;> simp
 
-/-! ### Decidability of bounded quantifiers -/
-
-instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    Decidable (∀ x, x ∈ xs → p x) :=
-  decidable_of_iff (∀ (i : Nat) h, p (xs[i]'h)) (by
-    simp only [mem_iff_getElem, forall_exists_index]
-    exact
-      ⟨by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl⟩)
-
-instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    Decidable (∃ x, x ∈ xs ∧ p x) :=
-  decidable_of_iff (∃ (i : Nat), ∃ (h : i < xs.size), p (xs[i]'h)) (by
-    simp [mem_iff_getElem]
-    exact
-      ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)
-
 /-! ### any / all -/
 
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
@@ -411,15 +389,14 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
     (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
   rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
-theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat)
-    (h : stop + 1 ≤ (a :: as).length) :
-    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) =
-      anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
+theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) :
+    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) = anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
   rw [anyM.loop]
   conv => rhs; rw [anyM.loop]
   split <;> rename_i h'
   · simp only [Nat.add_lt_add_iff_right] at h'
-    rw [dif_pos h', anyM_loop_cons]
+    rw [dif_pos h']
+    rw [anyM_loop_cons]
     simp
   · rw [dif_neg]
     omega
@@ -474,15 +451,10 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
     · rintro ⟨i, hi, ge, _, h⟩
       exact ⟨i, by omega, by omega, by omega, h⟩
 
-@[simp] theorem any_eq_true {p : α → Bool} {as : Array α} :
-    as.any p = true ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
+theorem any_eq_true {p : α → Bool} {as : Array α} :
+    as.any p ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
   simp [any_iff_exists]
 
-@[simp] theorem any_eq_false {p : α → Bool} {as : Array α} :
-    as.any p = false ↔ ∀ (i : Nat) (_ : i < as.size), ¬p as[i] := by
-  rw [Bool.eq_false_iff, Ne, any_eq_true]
-  simp
-
 theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
@@ -513,15 +485,10 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
   simp only [any_iff_exists, Bool.not_eq_eq_eq_not, Bool.not_true, not_exists, not_and,
     Bool.not_eq_false, and_imp]
 
-@[simp] theorem all_eq_true {p : α → Bool} {as : Array α} :
-    as.all p = true ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
+theorem all_eq_true {p : α → Bool} {as : Array α} :
+    as.all p ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
   simp [all_iff_forall]
 
-@[simp] theorem all_eq_false {p : α → Bool} {as : Array α} :
-    as.all p = false ↔ ∃ (i : Nat) (_ : i < as.size), ¬p as[i] := by
-  rw [Bool.eq_false_iff, Ne, all_eq_true]
-  simp
-
 theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
@@ -534,346 +501,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
-theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.anyM p = l.anyM p := by
-  rw [← anyM_toList]
-
-theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [any_toList]
-
-theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.allM p = l.allM p := by
-  rw [← allM_toList]
-
-theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [all_toList]
-
-/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.anyM p 0 stop = l.anyM p := by
-  subst h
-  rw [← anyM_toList]
-
-/-- Variant of `any_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.any p 0 stop = l.any p := by
-  subst h
-  rw [any_toList]
-
-/-- Variant of `allM_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.allM p 0 stop = l.allM p := by
-  subst h
-  rw [← allM_toList]
-
-/-- Variant of `all_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.all p 0 stop = l.all p := by
-  subst h
-  rw [all_toList]
-
-/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
-theorem any_eq_true' {p : α → Bool} {as : Array α} :
-    as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
-  cases as
-  simp
-
-/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
-theorem any_eq_false' {p : α → Bool} {as : Array α} :
-    as.any p = false ↔ ∀ x, x ∈ as → ¬p x := by
-  rw [Bool.eq_false_iff, Ne, any_eq_true']
-  simp
-
-/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
-theorem all_eq_true' {p : α → Bool} {as : Array α} :
-    as.all p = true ↔ (∀ x, x ∈ as → p x) := by
-  cases as
-  simp
-
-/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
-theorem all_eq_false' {p : α → Bool} {as : Array α} :
-    as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x := by
-  rw [Bool.eq_false_iff, Ne, all_eq_true']
-  simp
-
-theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
-  by_cases h : xs.any p
-  · simp_all [any_eq_true]
-  · simp_all [any_eq_false]
-
-/-- Variant of `any_eq` in terms of membership rather than an array index. -/
-theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x) := by
-  by_cases h : xs.any p
-  · simp_all [any_eq_true', -any_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [any_eq_false'] at h
-    simpa using h
-
-theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i]) := by
-  by_cases h : xs.all p
-  · simp_all [all_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [all_eq_false] at h
-    simpa using h
-
-/-- Variant of `all_eq` in terms of membership rather than an array index. -/
-theorem all_eq' {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x) := by
-  by_cases h : xs.all p
-  · simp_all [all_eq_true', -all_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [all_eq_false'] at h
-    simpa using h
-
-theorem decide_exists_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    decide (∃ x, x ∈ xs ∧ p x) = xs.any p := by
-  simp [any_eq']
-
-theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    decide (∀ x, x ∈ xs → p x) = xs.all p := by
-  simp [all_eq']
-
-@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
-    l.toArray.contains a = l.contains a := by
-  simp [Array.contains, List.any_beq]
-
-@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
-    Array.elem a l.toArray = List.elem a l := by
-  simp [Array.elem]
-
-theorem any_beq [BEq α] {xs : Array α} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
-  cases xs
-  simp [List.any_beq]
-
-/-- Variant of `any_beq` with `==` reversed. -/
-theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Array α} :
-    (xs.any fun x => x == a) = xs.contains a := by
-  simp only [BEq.comm, any_beq]
-
-theorem all_bne [BEq α] {xs : Array α} : (xs.all fun x => a != x) = !xs.contains a := by
-  cases xs
-  simp [List.all_bne]
-
-/-- Variant of `all_bne` with `!=` reversed. -/
-theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
-    (xs.all fun x => x != a) = !xs.contains a := by
-  simp only [bne_comm, all_bne]
-
-theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true → a ∈ as := by
-  cases as
-  simp
-
-theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : elem a as = true := by
-  cases as
-  simpa using h
-
-instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
-
-@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
-    elem a l = l.contains a := by
-  simp [elem]
-
-theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
-    elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
-    as.contains a = decide (a ∈ as) := by rw [← elem_eq_contains, elem_eq_mem]
-
-/-- Variant of `any_push` with a side condition on `stop`. -/
-@[simp] theorem any_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
-    (as.push a).any p 0 stop = (as.any p || p a) := by
-  cases as
-  rw [List.push_toArray]
-  simp [h]
-
-theorem any_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
-    (as.push a).any p = (as.any p || p a) :=
-  any_push' (by simp)
-
-/-- Variant of `all_push` with a side condition on `stop`. -/
-@[simp] theorem all_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
-    (as.push a).all p 0 stop = (as.all p && p a) := by
-  cases as
-  rw [List.push_toArray]
-  simp [h]
-
-theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
-    (as.push a).all p = (as.all p && p a) :=
-  all_push' (by simp)
-
-@[simp] theorem contains_push [BEq α] {l : Array α} {a : α} {b : α} :
-    (l.push a).contains b = (l.contains b || b == a) := by
-  simp [contains]
-
-/-! ### set -/
-
-
-/-! # set -/
-
-@[simp] theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
-      (eq : i = j) (p : j < (a.set i v).size) :
-    (a.set i v)[j]'p = v := by
-  cases a
-  simp
-  simp [set, ← getElem_toList, ←eq]
-
-@[deprecated getElem_set_self (since := "2024-12-11")]
-abbrev getElem_set_eq := @getElem_set_self
-
-@[simp] theorem getElem?_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
-    (a.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
-
-@[deprecated getElem?_set_self (since := "2024-12-11")]
-abbrev getElem?_set_eq := @getElem?_set_self
-
-@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
-    (pj : j < (a.set i v).size) (h : i ≠ j) :
-    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]
-
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
-    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases h : j < a.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]
-
-theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
-    (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
-  by_cases p : i = j <;> simp [p]
-
-theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat) :
-    (a.set i v)[j]? = if i = j then some v else a[j]? := by
-  split <;> simp_all
-
-@[simp] theorem set_getElem_self {as : Array α} {i : Nat} (h : i < as.size) :
-    as.set i as[i] = as := by
-  cases as
-  simp
-
-@[simp] theorem set_eq_empty_iff {as : Array α} (n : Nat) (a : α) (h) :
-     as.set n a = #[] ↔ as = #[] := by
-  cases as <;> cases n <;> simp [set]
-
-theorem set_comm (a b : α)
-    {n m : Nat} (as : Array α) {hn : n < as.size} {hm : m < (as.set n a).size} (h : n ≠ m) :
-    (as.set n a).set m b = (as.set m b (by simpa using hm)).set n a (by simpa using hn) := by
-  cases as
-  simp [List.set_comm _ _ _ h]
-
-@[simp]
-theorem set_set (a b : α) (as : Array α) (n : Nat) (h : n < as.size) :
-    (as.set n a).set n b (by simpa using h) = as.set n b := by
-  cases as
-  simp
-
-theorem mem_set (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.set n a := by
-  simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
-
-theorem mem_or_eq_of_mem_set
-    {as : Array α} {n : Nat} {a b : α} {w : n < as.size} (h : a ∈ as.set n b) : a ∈ as ∨ a = b := by
-  cases as
-  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
-
-/-! # setIfInBounds -/
-
-@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
-
-@[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
-    (as.setIfInBounds index val).size = as.size := by
-  if h : index < as.size  then
-    simp [setIfInBounds, h]
-  else
-    simp [setIfInBounds, h]
-
-theorem getElem_setIfInBounds (as : Array α) (i : Nat) (v : α) (j : Nat)
-    (hj : j < (as.setIfInBounds i v).size) :
-    (as.setIfInBounds i v)[j]'hj = if i = j then v else as[j]'(by simpa using hj) := by
-  simp only [setIfInBounds]
-  split
-  · simp [getElem_set]
-  · simp only [size_setIfInBounds] at hj
-    rw [if_neg]
-    omega
-
-@[simp] theorem getElem_setIfInBounds_self (as : Array α) {i : Nat} (v : α) (h : _) :
-    (as.setIfInBounds i v)[i]'h = v := by
-  simp at h
-  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]
-
-@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
-
-@[simp] theorem getElem_setIfInBounds_ne (as : Array α) {i : Nat} (v : α) {j : Nat}
-    (hj : j < (as.setIfInBounds i v).size) (h : i ≠ j) :
-    (as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
-  simp [getElem_setIfInBounds, h]
-
-@[simp]
-theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (p : i < as.size) (v : α) :
-    (as.setIfInBounds i v)[i]? = some v := by
-  simp [getElem?_eq_getElem, p]
-
-@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
-
-theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
-    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
-  cases as
-  simp [List.getElem?_set]
-
-@[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
-    (as.setIfInBounds i a)[j]? = as[j]? := by
-  simp [getElem?_setIfInBounds, h]
-
-theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n) {a : α} :
-    l.setIfInBounds n a = l := by
-  cases l
-  simp [List.set_eq_of_length_le (by simpa using h)]
-
-@[simp] theorem setIfInBounds_eq_empty_iff {as : Array α} (n : Nat) (a : α) :
-     as.setIfInBounds n a = #[] ↔ as = #[] := by
-  cases as <;> cases n <;> simp
-
-theorem setIfInBounds_comm (a b : α)
-    {n m : Nat} (as : Array α) (h : n ≠ m) :
-    (as.setIfInBounds n a).setIfInBounds m b = (as.setIfInBounds m b).setIfInBounds n a := by
-  cases as
-  simp [List.set_comm _ _ _ h]
-
-@[simp]
-theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (n : Nat) :
-    (as.setIfInBounds n a).setIfInBounds n b = as.setIfInBounds n b := by
-  cases as
-  simp
-
-theorem mem_setIfInBounds (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.setIfInBounds n a := by
-  simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
-
-theorem mem_or_eq_of_mem_setIfInBounds
-    {as : Array α} {n : Nat} {a b : α} (h : a ∈ as.setIfInBounds n b) : a ∈ as ∨ a = b := by
-  cases as
-  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
-
-/-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
-    (setIfInBounds a i v)[i]?.getD d = if i < a.size then v else d := by
-  by_cases h : i < a.size <;>
-    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
-
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -984,31 +611,102 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
 
 @[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_eq_none, h]
+  simp [getElem?_ge, h]
 
-@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
+theorem getD_get? (a : Array α) (i : Nat) (d : α) :
+  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
+  if h : i < a.size then
+    simp [setIfInBounds, h, getElem?_def]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [setIfInBounds, getElem?_len_le _ p, h]
 
 @[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
+  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
     a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
+  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
+
+/-! # set -/
+
+@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
+    (a.set i v)[j]'p = v := by
+  cases a
+  simp
+  simp [set, ← getElem_toList, ←eq]
+
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]
+
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
+    (h : j < (a.set i v).size) :
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
+
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
+
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
+
+/-! # setIfInBounds -/
+
+@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
+
+@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
+    (Array.setIfInBounds a index val).size = a.size := by
+  if h : index < a.size  then
+    simp [setIfInBounds, h]
+  else
+    simp [setIfInBounds, h]
+
+theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (j : Nat)
+    (hj : j < (setIfInBounds a i v).size) :
+  (setIfInBounds a i v)[j]'hj = if i = j then v else a[j]'(by simpa using hj) := by
+  simp only [setIfInBounds]
+  split
+  · simp [getElem_set]
+  · simp only [size_setIfInBounds] at hj
+    rw [if_neg]
+    omega
+
+@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
+    (setIfInBounds a i v)[i]'h = v := by
+  simp at h
+  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
+
+@[simp] theorem getElem_setIfInBounds_ne (a : Array α) {i : Nat} (v : α) {j : Nat}
+    (hj : j < (setIfInBounds a i v).size) (h : i ≠ j) :
+    (setIfInBounds a i v)[j]'hj = a[j]'(by simpa using hj) := by
+  simp [getElem_setIfInBounds, h]
+
+@[simp]
+theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
+    (a.setIfInBounds i v)[i]? = some v := by
+  simp [getElem?_lt, p]
+
+/-- Simplifies a normal form from `get!` -/
+@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
+    Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
+  by_cases h : i < a.size <;>
+    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_get?]
 
 /-! # ofFn -/
 
@@ -1185,6 +883,9 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
+theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
+    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
+
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
@@ -2088,6 +1789,54 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
+@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setIfInBounds]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
+theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [any_toList]
+
+theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [all_toList]
+
+/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
+@[simp] theorem anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.anyM p 0 stop = l.anyM p := by
+  subst h
+  rw [← anyM_toList]
+
+/-- Variant of `any_toArray` with a side condition on `stop`. -/
+@[simp] theorem any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.any p 0 stop = l.any p := by
+  subst h
+  rw [any_toList]
+
+/-- Variant of `allM_toArray` with a side condition on `stop`. -/
+@[simp] theorem allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.allM p 0 stop = l.allM p := by
+  subst h
+  rw [← allM_toList]
+
+/-- Variant of `all_toArray` with a side condition on `stop`. -/
+@[simp] theorem all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.all p 0 stop = l.all p := by
+  subst h
+  rw [all_toList]
+
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
@@ -2406,8 +2155,8 @@ abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
 @[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
-@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
-@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
+@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
+@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
 @[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
 @[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
 

src/Init/Data/BEq.lean

@@ -40,9 +40,6 @@ theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
-theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
-  rw [bne, BEq.comm, bne]
-
 theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
   BEq.comm (α := α) ▸ id
 

src/Init/Data/BitVec/Bitblast.lean

@@ -462,7 +462,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case true =>
         apply hmin
         apply eq_of_getMsbD_eq
-        intro i hi
+        rintro ⟨i, hi⟩
         simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]
         cases i
         case zero => exact hmsb
@@ -470,7 +470,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case false =>
         apply hzero
         apply eq_of_getMsbD_eq
-        intro i hi
+        rintro ⟨i, hi⟩
         simp only [getMsbD_zero]
         cases i
         case zero => exact hmsb
@@ -573,11 +573,11 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
-  · ext k h
-    simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  · ext k
+    simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
-      simp [h]
+      simp
     · simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]
       by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega

src/Init/Data/BitVec/Lemmas.lean

@@ -173,21 +173,21 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
 -- We choose `eq_of_getLsbD_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsbD_eq`.
 @[ext] theorem eq_of_getLsbD_eq {x y : BitVec w}
-    (pred : ∀ i, i < w → x.getLsbD i = y.getLsbD i) : x = y := by
+    (pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
   intro i
   if i_lt : i < w then
-    exact pred i i_lt
+    exact pred ⟨i, i_lt⟩
   else
     have p : i ≥ w := Nat.le_of_not_gt i_lt
     simp [testBit_toNat, getLsbD_ge _ _ p]
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
-    (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y := by
+    (pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := by
   simp only [getMsbD] at pred
   apply eq_of_getLsbD_eq
-  intro i i_lt
+  intro ⟨i, i_lt⟩
   if w_zero : w = 0 then
     simp [w_zero]
   else
@@ -199,7 +199,7 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
       simp only [Nat.sub_sub]
       apply Nat.sub_lt w_pos
       simp [Nat.succ_add]
-    have q := pred (w - 1 - i) q_lt
+    have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
 -- This cannot be a `@[simp]` lemma, as it would be tried at every term.
@@ -241,11 +241,8 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
 @[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
   cases b <;> rfl
 
-@[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
-  cases b <;> rfl
-
-@[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
-  cases b <;> rfl
+@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
+  cases b <;> simp [BitVec.msb, getMsbD, getLsbD]
 
 theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
   rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
@@ -369,12 +366,6 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
   · simp only [ofBool]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
-  cases b <;> simp [getMsbD]
-
-@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
-  cases b <;> simp [BitVec.msb]
-
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -507,9 +498,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 @[simp] theorem ofInt_ofNat (w n : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
-@[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
-  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]
-
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
   simp [toInt_eq_toNat_cond]; omega
@@ -581,10 +569,6 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
     (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
   simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
-@[simp] theorem toFin_setWidth {x : BitVec w} :
-    (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
-  ext; simp
-
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
   rw [toNat_setWidth, toNat_setWidth']
@@ -661,20 +645,6 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
   simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
 
-theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
-    getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
-  unfold setWidth
-  by_cases h : n ≤ m <;> simp only [h]
-  · by_cases h' : m - n ≤ i
-    <;> simp [h', show i - (m - n) = i + n - m by omega]
-  · simp only [show m - n = 0 by omega, getMsbD, getLsbD_setWidth]
-    by_cases h' : i < m
-    · simp [show m - 1 - i < m by omega, show i + n - m < n by omega,
-        show n - 1 - (i + n - m) = m - 1 - i by omega]
-      omega
-    · simp [h']
-      omega
-
 @[simp] theorem getMsbD_setWidth_add {x : BitVec w} (h : k ≤ i) :
     (x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by
   by_cases h : w = 0
@@ -719,15 +689,14 @@ theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k :
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
 theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
-  ext i h
-  simp at h
-  simp [getLsbD_setWidth, h]
+  ext i
+  simp [getLsbD_setWidth, Fin.fin_one_eq_zero i]
 
 /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
 theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
+  ext ⟨i, hilt⟩
+  simp only [getLsbD_setWidth, hilt, decide_true, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
   intros hi₁
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
@@ -754,7 +723,8 @@ protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
 @[simp]
 protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
-  ext i
+  apply eq_of_getLsbD_eq
+  intro ⟨i, _lt⟩
   simp [BitVec.ofNat]
 
 @[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
@@ -841,8 +811,8 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem setWidth_or {x y : BitVec w} :
     (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem or_assoc (x y z : BitVec w) :
     x ||| y ||| z = x ||| (y ||| z) := by
@@ -875,12 +845,12 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
   simp
 
 @[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 /-! ### and -/
 
@@ -914,8 +884,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
 
 @[simp] theorem setWidth_and {x y : BitVec w} :
     (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem and_assoc (x y z : BitVec w) :
     x &&& y &&& z = x &&& (y &&& z) := by
@@ -945,15 +915,15 @@ instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where
   simp
 
 @[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where
   right_id _ := BitVec.and_allOnes
 
 @[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 /-! ### xor -/
 
@@ -990,8 +960,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher
 
 @[simp] theorem setWidth_xor {x y : BitVec w} :
     (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem xor_assoc (x y z : BitVec w) :
     x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
@@ -1084,9 +1054,9 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   rw [Nat.testBit_two_pow_sub_succ x.isLt]
   simp [h]
 
-@[simp] theorem setWidth_not {x : BitVec w} (_ : k ≤ w) :
+@[simp] theorem setWidth_not {x : BitVec w} (h : k ≤ w) :
     (~~~x).setWidth k = ~~~(x.setWidth k) := by
-  ext i h
+  ext
   simp [h]
   omega
 
@@ -1099,17 +1069,17 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp
 
 @[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp]
 theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
@@ -1184,21 +1154,24 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_xor]
+  by_cases h : i < n
+    <;> simp [h]
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_and]
+  by_cases h : i < n
+    <;> simp [h]
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or]
+  by_cases h : i < n
+    <;> simp [h]
 
 @[simp] theorem getMsbD_shiftLeft (x : BitVec w) (i) :
     (x <<< i).getMsbD k = x.getMsbD (k + i) := by
@@ -1537,12 +1510,12 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
-  ext i h
-  simp [getLsbD_sshiftRight, h]
+  ext i
+  simp [getLsbD_sshiftRight]
 
 @[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
-  ext i h
-  simp [getLsbD_sshiftRight, h]
+  ext i
+  simp [getLsbD_sshiftRight]
 
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
@@ -1643,7 +1616,7 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
     -(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl
 
 /-- The sign extension is the same as zero extending when `msb = false`. -/
-theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
+theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
@@ -1679,36 +1652,21 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
 theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · rw [signExtend_eq_setWidth_of_msb_false hmsb]
+  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
-theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
-    (x.signExtend v).getMsbD i =
-      (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb) := by
-  rcases hmsb : x.msb with rfl | rfl
-  · simp only [signExtend_eq_setWidth_of_msb_false hmsb, getMsbD_setWidth]
-    by_cases h : v - w ≤ i <;> simp [h, getMsbD] <;> omega
-  · simp only [signExtend_eq_not_setWidth_not_of_msb_true hmsb, getMsbD_not, getMsbD_setWidth]
-    by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega
-
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
   rw [←getLsbD_eq_getElem, getLsbD_signExtend]
   simp [h]
 
-theorem msb_signExtend {x : BitVec w} :
-    (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by
-  by_cases h : w ≥ v
-  · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
-  · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
-
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
-  ext i h
-  simp only [getLsbD_signExtend, h, decide_true, Bool.true_and, getLsbD_setWidth,
+  ext i
+  simp only [getLsbD_signExtend, Fin.is_lt, decide_true, Bool.true_and, getLsbD_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -1802,34 +1760,35 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
   rfl
 
 theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
-    getLsbD (x ++ y) i = if i < m then getLsbD y i else getLsbD x (i - m) := by
+    getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
   · simp_all [h]
 
 theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
-    (x ++ y)[i] = if i < m then getLsbD y i else getLsbD x (i - m) := by
+    (x ++ y)[i] = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
   by_cases h' : i < m
   · simp [h']
   · simp_all [h']
 
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
-    getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i := by
+    getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
   simp only [append_def]
   by_cases h : n ≤ i
   · simp [h]
   · simp [h]
 
 theorem msb_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).msb = if w = 0 then y.msb else x.msb := by
+    (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
   simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth']
   by_cases h : w = 0
   · subst h
     simp [BitVec.msb, getMsbD]
-  · have q : 0 < w + v := by omega
+  · rw [cond_eq_if]
+    have q : 0 < w + v := by omega
     have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
     simp [h, q, t, BitVec.msb, getMsbD]
 
@@ -1845,7 +1804,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 @[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
   ext
-  simp only [getLsbD_append, getLsbD_zero, ite_self]
+  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) :
     (x ++ y).cast h = x ++ y.cast (by omega) := by
@@ -1865,19 +1824,21 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
-  ext i h
-  simp only [getLsbD_setWidth, h, getLsbD_append]
-  split <;> rename_i h₁ <;> split <;> rename_i h₂
-  · simp [h]
-  · simp [getLsbD_append, h₁]
-  · omega
-  · simp [getLsbD_append, h₁]
-    omega
+  apply eq_of_getLsbD_eq
+  intro i
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, Bool.true_and]
+  split
+  · have t : i < v := by omega
+    simp [t]
+  · by_cases t : i < v
+    · simp [t, getLsbD_append]
+    · have t' : i - v < k - v := by omega
+      simp [t, t', getLsbD_append]
 
 @[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_append, cond_eq_if,
+  ext i
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, cond_eq_if,
     decide_eq_true_eq, Bool.true_and, setWidth_eq]
   split
   · simp_all
@@ -1927,12 +1888,12 @@ theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
   case succ n ih =>
     rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
        Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]
-    ext i h
+    ext i
     by_cases hw : w = 0
     · simp [hw]
-    · by_cases hi₂ : i = 0
+    · by_cases hi₂ : i.val = 0
       · simp [hi₂]
-      · simp [Nat.lt_one_iff, hi₂, h, show 1 + (i - 1) = i by omega]
+      · simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
 
 @[simp]
 theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
@@ -2017,12 +1978,13 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
 
 theorem setWidth_succ (x : BitVec w) :
     setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
-  ext j h
-  simp only [getLsbD_setWidth, getLsbD_cons, h, decide_true, Bool.true_and]
-  if j_eq : j = i then
+  apply eq_of_getLsbD_eq
+  intro j
+  simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_true, Bool.true_and]
+  if j_eq : j.val = i then
     simp [j_eq]
   else
-    have j_lt : j < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ h) j_eq
+    have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
 @[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
@@ -2136,19 +2098,19 @@ theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
   simp [← Fin.val_inj]
 
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
 
 @[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
   ext
@@ -2169,8 +2131,8 @@ theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
 
 theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
     n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
-  ext i h
-  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, h, decide_true, Bool.true_and]
+  ext i
+  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_true, Bool.true_and]
   split
   · simp [*]
   · congr 1; omega
@@ -3181,8 +3143,8 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
   {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) := by
-  ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -3197,17 +3159,20 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) ||| (twoPow w i) := by
-  ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
-    simp [hx, h]
+    simp [hx]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
 /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
 theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
     (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
-  ext (_ | i) h <;> simp [Bool.and_comm]
+  ext i
+  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_ofBool,
+    Bool.true_and]
+  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
@@ -3231,7 +3196,7 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
       · simp [hi', ih]
-      · simp [hi', decide_false]
+      · simp only [hi', decide_false, cond_false]
         rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
     · rw [Nat.mul_succ] at hi ⊢
       simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
@@ -3537,7 +3502,7 @@ theorem forall_zero_iff {P : BitVec 0 → Prop} :
   · intro h
     apply h
   · intro h v
-    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
     apply h
 
 theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
@@ -3553,7 +3518,7 @@ theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
 instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
     ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
   | .isTrue h => .isTrue fun v => by
-    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
     exact h
   | .isFalse h => .isFalse (fun w => h (w _))
 
@@ -3598,9 +3563,6 @@ instance instDecidableExistsBitVec :
 
 set_option linter.missingDocs false
 
-@[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
-abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
-
 @[deprecated truncate_eq_setWidth (since := "2024-09-18")]
 abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
 
@@ -3703,8 +3665,8 @@ abbrev truncate_xor := @setWidth_xor
 @[deprecated setWidth_not (since := "2024-09-18")]
 abbrev truncate_not := @setWidth_not
 
-@[deprecated signExtend_eq_setWidth_of_msb_false  (since := "2024-09-18")]
-abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth_of_msb_false
+@[deprecated signExtend_eq_not_setWidth_not_of_msb_false  (since := "2024-09-18")]
+abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_not_setWidth_not_of_msb_false
 
 @[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
 abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true

src/Init/Data/List/Basic.lean

@@ -666,14 +666,10 @@ def isEmpty : List α → Bool
 /-! ### elem -/
 
 /--
-`O(|l|)`.
-`l.contains a` or `elem a l` is true if there is an element in `l` equal (according to `==`) to `a`.
+`O(|l|)`. `elem a l` or `l.contains a` is true if there is an element in `l` equal to `a`.
 
-* `[1, 4, 2, 3, 3, 7].contains 3 = true`
-* `[1, 4, 2, 3, 3, 7].contains 5 = false`
-
-The preferred simp normal form is `l.contains a`, and when `LawfulBEq α` is available,
-`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.
+* `elem 3 [1, 4, 2, 3, 3, 7] = true`
+* `elem 5 [1, 4, 2, 3, 3, 7] = false`
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false

src/Init/Data/List/Lemmas.lean

@@ -253,14 +253,6 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
-    l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
-  if h : i < l.length then
-    simp [h, getElem?_def]
-  else
-    have p : i ≥ l.length := Nat.le_of_not_gt h
-    simp [getElem?_eq_none p, h]
-
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
 theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
@@ -459,10 +451,6 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
         simp only [getElem_cons_succ]
         exact getElem_mem (lt_of_succ_lt_succ h)
 
-@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
-    elem a l = l.contains a := by
-  simp [contains]
-
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
@@ -470,20 +458,9 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
-theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
-    as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-@[simp] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
-    (a :: l).contains b = (b == a || l.contains b) := by
-  simp only [contains, elem_cons]
-  split <;> simp_all
-
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
@@ -528,21 +505,17 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
-  induction l <;> simp_all [contains_cons]
+theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
+  simp
 
-/-- Variant of `any_beq` with `==` reversed. -/
-theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
-    (l.any fun x => x == a) = l.contains a := by
-  simp only [BEq.comm, any_beq]
+theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
+  simp
 
-theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
-  induction l <;> simp_all [bne]
+theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
+  induction l <;> simp_all
 
-/-- Variant of `all_bne` with `!=` reversed. -/
-theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
-    (l.all fun x => x != a) = !l.contains a := by
-  simp only [bne_comm, all_bne]
+theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
+  induction l <;> simp_all [eq_comm (a := a)]
 
 /-! ### set -/
 
@@ -2855,6 +2828,11 @@ theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l)
 
 theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
+@[simp] theorem contains_cons [BEq α] :
+    (a :: as : List α).contains x = (x == a || as.contains x) := by
+  simp only [contains, elem]
+  split <;> simp_all
+
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 

src/Init/Data/List/ToArray.lean

@@ -363,12 +363,4 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
-    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
-  apply ext'
-  simp only [setIfInBounds]
-  split
-  · simp
-  · simp_all [List.set_eq_of_length_le]
-
 end List

src/Init/Data/Nat/Lemmas.lean

@@ -1046,25 +1046,6 @@ instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Na
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
 
-/-- Dependent version of `decidableExistsLT`. -/
-instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Decidable (p m h)] :
-    Decidable (∃ m : Nat, ∃ h : m < k, p m h) :=
-  match k, p, I with
-  | 0, _, _ => isFalse (by simp)
-  | (k + 1), p, I => @decidable_of_iff _ ((∃ m, ∃ h : m < k, p m (by omega)) ∨ p k (by omega))
-      ⟨by rintro (⟨m, h, w⟩ | w); exact ⟨m, by omega, w⟩; exact ⟨k, by omega, w⟩,
-        fun ⟨m, h, w⟩ => if h' : m < k then .inl ⟨m, h', w⟩ else
-          by obtain rfl := (by omega : m = k); exact .inr w⟩
-      (@instDecidableOr _ _
-        (decidableExistsLT' (p := fun m h => p m (by omega)) (I := fun m h => I m (by omega)))
-        inferInstance)
-
-/-- Dependent version of `decidableExistsLE`. -/
-instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
-    Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
-  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
-    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
-
 /-! ### Results about `List.sum` specialized to `Nat` -/
 
 protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by

src/Lean/Elab/PreDefinition/Main.lean

@@ -22,8 +22,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
       let value ← if useSorry then
         mkLambdaFVars xs (← mkSorry type (synthetic := true))
       else
-        let msg := m!"failed to compile 'partial' definition '{preDef.declName}'"
-        liftM <| mkInhabitantFor msg xs type
+        liftM <| mkInhabitantFor preDef.declName xs type
       addNonRec { preDef with
         kind  := DefKind.«opaque»
         value

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -50,13 +50,13 @@ private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (u
       return none
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-def mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Expr) : MetaM Expr :=
+def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
   withInhabitedInstances xs fun insts => do
     if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts type true then
       return val
     else
       throwError "\
-        {failedToMessage}, could not prove that the type\
+        failed to compile 'partial' definition '{declName}', could not prove that the type\
         {indentExpr (← mkForallFVars xs type)}\n\
         is nonempty.\n\
         \n\

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -20,7 +20,6 @@ structure EqnInfo extends EqnInfoCore where
   declNameNonRec  : Name
   fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
-  hasInduct       : Bool
   deriving Inhabited
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -102,7 +101,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
-    (argsPacker : ArgsPacker) (hasInduct : Bool) : MetaM Unit := do
+    (argsPacker : ArgsPacker) : MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -115,7 +114,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker, hasInduct }
+            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -178,8 +178,7 @@ def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Arr
     let type ← goal.getType
     let (.mdata _ (.app _ param)) := type
         | throwError "MVar does not look like a recursive call:{indentExpr type}"
-    let some (funidx, _) := argsPacker.unpack param
-        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
+    let (funidx, _) ← argsPacker.unpack param
     r := r.modify funidx (·.push goal)
   return r
 

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -352,10 +352,8 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
-      let some (caller, params) := argsPacker.unpack param
-        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
-      let some (callee, args) := argsPacker.unpack arg
-        | throwError "Cannot unpack arg, unexpected expression:{indentExpr arg}"
+      let (caller, params) ← argsPacker.unpack param
+      let (callee, args) ← argsPacker.unpack arg
       RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
 
 /-- Is the expression a `<`-like comparison of `Nat` expressions -/
@@ -773,8 +771,6 @@ Main entry point of this module:
 
 Try to find a lexicographic ordering of the arguments for which the recursive definition
 terminates. See the module doc string for a high-level overview.
-
-The `preDefs` are used to determine arity and types of arguments; the bodies are ignored.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -110,7 +110,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
     unless type.isForall do
       throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
@@ -142,7 +142,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker (hasInduct := true)
+  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
     markAsRecursive preDef.declName
     generateEagerEqns preDef.declName

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -51,12 +51,12 @@ If the `termArgs` map the packed argument `argType` to `β`, then this function
 continuation a value of type `WellFoundedRelation argType` that is derived from the instance
 for `WellFoundedRelation β` using `invImage`.
 -/
-def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr)
+def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
     (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
     (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains declNames prefixArgs argsPacker.arities termArgs
+  let β ← checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
   let v ← getLevel β
   let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
   let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)

src/Lean/Meta/ArgsPacker.lean

@@ -87,7 +87,7 @@ Unpacks a unary packed argument created with `Unary.pack`.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do
+def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do
   let mut e := e
   let mut args := #[]
   while args.size + 1 < arity do
@@ -95,10 +95,11 @@ def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do
       args := args.push (e.getArg! 2)
       e := e.getArg! 3
     else
-      none
+      throwError "Unexpected expression while unpacking n-ary argument"
   args := args.push e
   return args
 
+
 /--
   Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
   Return an array containing its "elements".
@@ -257,7 +258,7 @@ argument and function index.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr) := do
+def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do
   let mut funidx := 0
   let mut e := expr
   while funidx + 1 < numFuncs do
@@ -268,7 +269,7 @@ def unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr) := do
       e := e.getArg! 2
       break
     else
-      none
+      throwError "Unexpected expression while unpacking mutual argument:{indentExpr expr}"
   return (funidx, e)
 
 
@@ -376,17 +377,14 @@ and `(z : C) → R₂[z]`, returns an expression of type
 (x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z])
 ```
 -/
-def uncurryWithType (resultType : Expr) (es : Array Expr) : MetaM Expr := do
+def uncurry (es : Array Expr) : MetaM Expr := do
+  let types ← es.mapM inferType
+  let resultType ← uncurryType types
   forallBoundedTelescope resultType (some 1) fun xs codomain => do
     let #[x] := xs | unreachable!
     let value ← casesOn x codomain es.toList
     mkLambdaFVars #[x] value
 
-def uncurry (es : Array Expr) : MetaM Expr := do
-  let types ← es.mapM inferType
-  let resultType ← uncurryType types
-  uncurryWithType resultType es
-
 /--
 Given unary expressions `e₁`, `e₂` with types `(x : A) → R`
 and `(z : C) → R`, returns an expression of type
@@ -416,7 +414,7 @@ def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do
 
 end Mutual
 
--- Now for the main definitions in this module
+-- Now for the main definitions in this moduleo
 
 /-- The number of functions being packed -/
 def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
@@ -424,10 +422,6 @@ def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
 /-- The arities of the functions being packed -/
 def arities (argsPacker : ArgsPacker) : Array Nat := argsPacker.varNamess.map (·.size)
 
-def onlyOneUnary (argsPacker : ArgsPacker) :=
-  argsPacker.varNamess.size = 1 &&
-  argsPacker.varNamess[0]!.size = 1
-
 def pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr)
     : MetaM Expr := do
   assert! fidx < argsPacker.numFuncs
@@ -442,13 +436,14 @@ return the function index that is called and the arguments individually.
 
 We expect precisely the expressions produced by `pack`, with manifest
 `PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
-rather than using projections.
+rather than using projectinos.
 -/
-def unpack (argsPacker : ArgsPacker) (e : Expr) : Option (Nat × Array Expr) := do
+def unpack (argsPacker : ArgsPacker) (e : Expr) : MetaM (Nat × Array Expr) := do
   let (funidx, e) ← Mutual.unpack argsPacker.numFuncs e
   let args ← Unary.unpack argsPacker.varNamess[funidx]!.size e
   return (funidx, args)
 
+
 /--
 Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, returns the type uncurried type
 ```
@@ -470,10 +465,6 @@ def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do
   let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
   Mutual.uncurry unary
 
-def uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr := do
-  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
-  Mutual.uncurryWithType resultType unary
-
 /--
 Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R`
 and `(z : C) → R`, returns an expression of type

src/Lean/Meta/Tactic/FunInd.lean

@@ -810,8 +810,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
       let args := e.getAppArgs
       if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
         let packedArg := args.back!
-          let some (i, unpackedArgs) := eqnInfo.argsPacker.unpack packedArg
-            | throwError "Unexpected packedArg:{indentExpr packedArg}"
+          let (i, unpackedArgs) ← eqnInfo.argsPacker.unpack packedArg
           let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
           let e' := mkAppN e' args.pop
           let e' := mkAppN e' unpackedArgs
@@ -1111,16 +1110,11 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   match s with
   | "induct" =>
-    if let some eqnInfo := WF.eqnInfoExt.find? env p then
-      unless eqnInfo.hasInduct do
-        return false
-      return true
+    if (WF.eqnInfoExt.find? env p).isSome then return true
     if (Structural.eqnInfoExt.find? env p).isSome then return true
     return false
   | "mutual_induct" =>
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
-      unless eqnInfo.hasInduct do
-        return false
       if h : eqnInfo.declNames.size > 1 then
         return eqnInfo.declNames[0] = p
     if let some eqnInfo := Structural.eqnInfoExt.find? env p then

src/Lean/ResolveName.lean

@@ -398,22 +398,16 @@ Aliases are considered first.
 
 When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
 
-When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out.
-The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
-"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
-
 This function is meant to be used for pretty printing.
 If `n₀` is an accessible name, then the result will be an accessible name.
 -/
-def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
+def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
     match (← resolveGlobalName n₀) with
       | [(potentialMatch, _)] => if (privateToUserName? potentialMatch).getD potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀
       | _ => return n₀ -- if can't resolve, return the original
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
-  unless allowHorizAliases do
-    initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₀.getPrefix
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     if let some n ← unresolveNameCore initialName then

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -77,8 +77,12 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
       BitVec.getLsbD_append]
     split
-    · next hsplit => rw [rih]
-    · next hsplit => rw [go_denote_mem_prefix, lih]
+    · next hsplit =>
+      simp only [hsplit, decide_true, cond_true]
+      rw [rih]
+    · next hsplit =>
+      simp only [hsplit, decide_false, cond_false]
+      rw [go_denote_mem_prefix, lih]
   | replicate n expr ih => simp [go, ih, hidx]
   | signExtend v inner ih =>
     rename_i originalWidth
@@ -91,7 +95,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
       rw [blastSignExtend_empty_eq_zeroExtend] at hgo
       · rw [← hgo]
         simp only [eval_signExtend]
-        rw [BitVec.signExtend_eq_setWidth_of_msb_false]
+        rw [BitVec.signExtend_eq_not_setWidth_not_of_msb_false]
         · simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
             BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp,
             decide_eq_true_eq]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean

@@ -30,9 +30,9 @@ theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign :
   simp only [RefVec.denote_fold_and, RefVec.denote_zip, denote_mkBEqCached, beq_iff_eq]
   constructor
   · intro h
-    ext i h'
+    ext
     rw [← hleft, ← hright]
-    · simp [h, h']
+    · simp [h]
     · omega
     · omega
   · intro h idx hidx

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

@@ -168,13 +168,13 @@ attribute [bv_normalize] BitVec.and_self
 
 @[bv_normalize]
 theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 @[bv_normalize]
 theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 @[bv_normalize]
 theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w) := by

tests/lean/run/5689.lean

@@ -1,17 +0,0 @@
-/-!
-# Pretty printing shouldn't make use of "non-API exports"
--/
-
-namespace A
-def n : Nat := 22
-end A
-
-namespace B
-export A (n)
-end B
-
-/-!
-Was `B.n`
--/
-/-- info: A.n : Nat -/
-#guard_msgs in #check (A.n)

tests/lean/run/DVec.lean

@@ -41,7 +41,7 @@ example (v : Vec Nat 1) : Nat :=
 -- Does not work: Aliases find that `v` could be the `TypeVec` argument since `TypeVec` is an abbrev for `Vec`.
 /--
 error: application type mismatch
-  @DVec.hd ?_ v
+  @Vec.hd ?_ v
 argument
   v
 has type

tests/lean/run/alias.lean

@@ -26,7 +26,7 @@ However, this dot notation fails since there is no `FinSet` argument.
 However, unfolding is the preferred method.
 -/
 /--
-error: invalid field notation, function 'Set.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
+error: invalid field notation, function 'FinSet.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
 -/
 #guard_msgs in
 example (x y : FinSet 10) : FinSet 10 :=

tests/lean/run/bv_uninterpreted.lean

@@ -5,8 +5,8 @@ example {x y z : BitVec w} :
     (x &&& y) ||| (x &&& z) ||| (y &&& z) ||| x ||| y ||| z
       =
     ~~~ ((~~~ x) &&& (~~~ y) &&& (~~~ z)) := by
-  ext i h
-  simp [h]
+  ext
+  simp
   bv_decide
 
 @[irreducible]

tests/lean/run/wfOverapplicationIssue.lean

@@ -1,6 +1,6 @@
 theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by
   simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
-  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
+  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
     unfold anyM.loop
     intro h
     split at h