feat: HashSet.ofArray (unverified)

We add some documentation explaining the auxiliary function in the
definition of `groupBy`. This has been moved here from Mathlib PR
[16818](https://github.com/leanprover-community/mathlib4/pull/16818) by
request of @semorrison.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

src/Init/Control/Basic.lean

@@ -28,7 +28,7 @@ Important instances include
 * `Option`, where `failure := none` and `<|>` returns the left-most `some`.
 * Parser combinators typically provide an `Applicative` instance for error-handling and
   backtracking.
-  
+
 Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add

src/Init/Data/Array/Lemmas.lean

@@ -828,7 +828,7 @@ theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.
     (as ++ bs)[i] = bs[i - as.size] := by
   simp only [getElem_eq_toList_getElem]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
-  conv => rhs; rw [← List.getElem_append_right (h' := h') (h := Nat.not_lt_of_ge hle)]
+  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [append_toList]
 
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by

src/Init/Data/BitVec/Basic.lean

@@ -64,7 +64,7 @@ protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
 /-- The `BitVec` with value `i mod 2^n`. -/
 @[match_pattern]
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin := Fin.ofNat' i (Nat.two_pow_pos n)
+  toFin := Fin.ofNat' (2^n) i
 
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩

src/Init/Data/BitVec/Lemmas.lean

@@ -31,13 +31,13 @@ namespace BitVec
   simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
   omega
 
-theorem lt_of_getLsbD (x : BitVec w) (i : Nat) : getLsbD x i = true → i < w := by
+theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w := by
   if h : i < w then
     simp [h]
   else
     simp [Nat.ge_of_not_lt h]
 
-theorem lt_of_getMsbD (x : BitVec w) (i : Nat) : getMsbD x i = true → i < w := by
+theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w := by
   if h : i < w then
     simp [h]
   else
@@ -245,7 +245,7 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 @[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
-@[simp] theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat' x (Nat.two_pow_pos w) := rfl
+@[simp] theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat' (2^w) x := rfl
 
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
 -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
@@ -546,7 +546,7 @@ theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsbD k :=
     (x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
   ext i
   simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
-  have p := lt_of_getLsbD x i
+  have p := lt_of_getLsbD (x := x) (i := i)
   revert p
   cases getLsbD x i <;> simp; omega
 
@@ -592,6 +592,12 @@ theorem truncate_one {x : BitVec w} :
   ext i
   simp [show i = 0 by omega]
 
+@[simp] theorem truncate_ofNat_of_le (h : v ≤ w) (x : Nat) : truncate v (BitVec.ofNat w x) = BitVec.ofNat v x := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [toNat_truncate, toNat_ofNat]
+  rw [Nat.mod_mod_of_dvd]
+  exact Nat.pow_dvd_pow_iff_le_right'.mpr h
+
 /-! ## extractLsb -/
 
 @[simp]
@@ -826,7 +832,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   BitVec.toNat_ofNat _ _
 
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
-    BitVec.toFin (x <<< n) = Fin.ofNat' (x.toNat <<< n) (Nat.two_pow_pos w) := rfl
+    BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
 @[simp]
 theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
@@ -1027,7 +1033,7 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
     · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self,
         decide_eq_true_eq]
       intros hlsb
-      apply BitVec.lt_of_getLsbD _ _ hlsb
+      apply BitVec.lt_of_getLsbD hlsb
   · by_cases hi : i ≥ w
     · simp [hi]
     · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and,
@@ -1228,7 +1234,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem zero_width_append (x : BitVec 0) (y : BitVec v) : x ++ y = cast (by omega) y := by
   ext
   rw [getLsbD_append]
-  simpa using lt_of_getLsbD _ _
+  simpa using lt_of_getLsbD
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = x ++ cast (by omega) y := by
@@ -1259,6 +1265,18 @@ theorem truncate_append {x : BitVec w} {y : BitVec v} :
     · have t' : i - v < k - v := by omega
       simp [t, t']
 
+@[simp] theorem truncate_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : truncate (v' + w') (x ++ y) = truncate v' x ++ truncate w' y := by
+  subst h
+  ext i
+  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_append, cond_eq_if,
+    decide_eq_true_eq, Bool.true_and, zeroExtend_eq]
+  split
+  · simp_all
+  · simp_all only [Bool.iff_and_self, decide_eq_true_eq]
+    intro h
+    have := BitVec.lt_of_getLsbD h
+    omega
+
 @[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
   simp [cons, truncate_append]
 
@@ -1508,7 +1526,7 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
   simp [Neg.neg, BitVec.neg]
 
 @[simp] theorem toFin_neg (x : BitVec n) :
-    (-x).toFin = Fin.ofNat' (2^n - x.toNat) (Nat.two_pow_pos _) :=
+    (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
   rfl
 
 theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by

src/Init/Data/Bool.lean

@@ -6,16 +6,11 @@ Authors: F. G. Dorais
 prelude
 import Init.NotationExtra
 
-/-- Boolean exclusive or -/
-abbrev xor : Bool → Bool → Bool := bne
 
 namespace Bool
 
-/- Namespaced versions that can be used instead of prefixing `_root_` -/
-@[inherit_doc not] protected abbrev not := not
-@[inherit_doc or]  protected abbrev or  := or
-@[inherit_doc and] protected abbrev and := and
-@[inherit_doc xor] protected abbrev xor := xor
+/-- Boolean exclusive or -/
+abbrev xor : Bool → Bool → Bool := bne
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
@@ -597,7 +592,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
 
 end Bool
 
-export Bool (cond_eq_if)
+export Bool (cond_eq_if xor and or not)
 
 /-! ### decide -/
 

src/Init/Data/Fin/Basic.lean

@@ -31,7 +31,7 @@ This differs from addition, which wraps around:
 (2 : Fin 3) + 1 = (0 : Fin 3)
 ```
 -/
-def succ : Fin n → Fin n.succ
+def succ : Fin n → Fin (n + 1)
   | ⟨i, h⟩ => ⟨i+1, Nat.succ_lt_succ h⟩
 
 variable {n : Nat}
@@ -39,16 +39,20 @@ variable {n : Nat}
 /--
 Returns `a` modulo `n + 1` as a `Fin n.succ`.
 -/
-protected def ofNat {n : Nat} (a : Nat) : Fin n.succ :=
+protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
   ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
 
 /--
 Returns `a` modulo `n` as a `Fin n`.
 
-The assumption `n > 0` ensures that `Fin n` is nonempty.
+The assumption `NeZero n` ensures that `Fin n` is nonempty.
 -/
-protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
-  ⟨a % n, Nat.mod_lt _ h⟩
+protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
+  ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
+
+-- We intend to deprecate `Fin.ofNat` in favor of `Fin.ofNat'` (and later rename).
+-- This is waiting on https://github.com/leanprover/lean4/pull/5323
+-- attribute [deprecated Fin.ofNat' (since := "2024-09-16")] Fin.ofNat
 
 private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
   | 0,   h => Nat.mod_lt _ h
@@ -141,10 +145,10 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin (no_index n)) i where
-  ofNat := Fin.ofNat' i (pos_of_neZero _)
+instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin n) i where
+  ofNat := Fin.ofNat' n i
 
-instance : Inhabited (Fin (no_index (n+1))) where
+instance instInhabited {n : Nat} [NeZero n] : Inhabited (Fin n) where
   default := 0
 
 @[simp] theorem zero_eta : (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0 := rfl

src/Init/Data/Fin/Lemmas.lean

@@ -51,10 +51,10 @@ theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
 
 theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 
-@[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
-  (Fin.ofNat' a is_pos).val = a % n := rfl
+@[simp] theorem val_ofNat' (n : Nat) [NeZero n] (a : Nat) :
+  (Fin.ofNat' n a).val = a % n := rfl
 
-@[simp] theorem ofNat'_val_eq_self (x : Fin n) (h) : (Fin.ofNat' x h) = x := by
+@[simp] theorem ofNat'_val_eq_self [NeZero n](x : Fin n) : (Fin.ofNat' n x) = x := by
   ext
   rw [val_ofNat', Nat.mod_eq_of_lt]
   exact x.2
@@ -750,13 +750,13 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 
 /-! ### add -/
 
-@[simp] theorem ofNat'_add (x : Nat) (lt : 0 < n) (y : Fin n) :
-    Fin.ofNat' x lt + y = Fin.ofNat' (x + y.val) lt := by
+@[simp] theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
+    Fin.ofNat' n x + y = Fin.ofNat' n (x + y.val) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.add_def]
 
-@[simp] theorem add_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
-    x + Fin.ofNat' y lt = Fin.ofNat' (x.val + y) lt := by
+@[simp] theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+    x + Fin.ofNat' n y = Fin.ofNat' n (x.val + y) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.add_def]
 
@@ -765,13 +765,13 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
   cases a; cases b; rfl
 
-@[simp] theorem ofNat'_sub (x : Nat) (lt : 0 < n) (y : Fin n) :
-    Fin.ofNat' x lt - y = Fin.ofNat' ((n - y.val) + x) lt := by
+@[simp] theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
+    Fin.ofNat' n x - y = Fin.ofNat' n ((n - y.val) + x) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
-@[simp] theorem sub_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
-    x - Fin.ofNat' y lt = Fin.ofNat' ((n - y % n) + x.val) lt := by
+@[simp] theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+    x - Fin.ofNat' n y = Fin.ofNat' n ((n - y % n) + x.val) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 

src/Init/Data/List/Attach.lean

@@ -48,6 +48,8 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 
 @[simp] theorem attach_nil : ([] : List α).attach = [] := rfl
 
+@[simp] theorem attachWith_nil : ([] : List α).attachWith P H = [] := rfl
+
 @[simp]
 theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) :
     @pmap _ _ p (fun a _ => f a) l H = map f l := by
@@ -81,7 +83,12 @@ theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
   subst h
   simp
 
-@[simp] theorem attach_cons (x : α) (xs : List α) :
+theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
+    l₁.attachWith P H = l₂.attachWith P fun x h => H _ (w ▸ h) := by
+  subst w
+  simp
+
+@[simp] theorem attach_cons {x : α} {xs : List α} :
     (x :: xs).attach =
       ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and]
@@ -89,6 +96,12 @@ theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
   intros a _ m' _
   rfl
 
+@[simp]
+theorem attachWith_cons {x : α} {xs : List α} {p : α → Prop} (h : ∀ a ∈ x :: xs, p a) :
+    (x :: xs).attachWith p h = ⟨x, h x (mem_cons_self x xs)⟩ ::
+      xs.attachWith p (fun a ha ↦ h a (mem_cons_of_mem x ha)) :=
+  rfl
+
 theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
     pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
   rw [attach, attachWith, map_pmap]; exact pmap_congr_left l fun _ _ _ _ => rfl
@@ -104,15 +117,37 @@ theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
   (attach_map_coe _ _).trans (List.map_id _)
 
+theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) :
+    ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
+  rw [attachWith, map_pmap]; exact pmap_eq_map _ _ _ _
+
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) :
+    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
+  attachWith_map_coe _ _ _
+
+@[simp]
+theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) :
+    (l.attachWith p H).map Subtype.val = l :=
+  (attachWith_map_coe _ _ _).trans (List.map_id _)
+
 theorem countP_attach (l : List α) (p : α → Bool) :
     l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
   simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]
 
+theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
+    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
+  simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]
+
 @[simp]
 theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) :
     l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
 
+@[simp]
+theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
+    (l.attachWith p H).count a = l.count ↑a :=
+  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
+
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
   | ⟨a, h⟩ => by
@@ -137,7 +172,11 @@ theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pm
   · simp only [*, pmap, length]
 
 @[simp]
-theorem length_attach (L : List α) : L.attach.length = L.length :=
+theorem length_attach {L : List α} : L.attach.length = L.length :=
+  length_pmap
+
+@[simp]
+theorem length_attachWith {p : α → Prop} {l H} : length (l.attachWith p H) = length l :=
   length_pmap
 
 @[simp]
@@ -155,6 +194,15 @@ theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] :=
 theorem attach_ne_nil_iff {l : List α} : l.attach ≠ [] ↔ l ≠ [] :=
   pmap_ne_nil_iff _ _
 
+@[simp]
+theorem attachWith_eq_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
+    l.attachWith P H = [] ↔ l = [] :=
+  pmap_eq_nil_iff
+
+theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
+    l.attachWith P H ≠ [] ↔ l ≠ [] :=
+  pmap_ne_nil_iff _ _
+
 @[deprecated pmap_eq_nil_iff (since := "2024-09-06")] abbrev pmap_eq_nil := @pmap_eq_nil_iff
 @[deprecated pmap_ne_nil_iff (since := "2024-09-06")] abbrev pmap_ne_nil := @pmap_ne_nil_iff
 @[deprecated attach_eq_nil_iff (since := "2024-09-06")] abbrev attach_eq_nil := @attach_eq_nil_iff
@@ -187,7 +235,7 @@ theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     (hn : n < (pmap f l h).length) :
     (pmap f l h)[n] =
       f (l[n]'(@length_pmap _ _ p f l h ▸ hn))
-        (h _ (getElem_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
+        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
   induction l generalizing n with
   | nil =>
     simp only [length, pmap] at hn
@@ -205,34 +253,26 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h :
   simp only [get_eq_getElem]
   simp [getElem_pmap]
 
+@[simp]
+theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
+    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (getElem?_mem a)) :=
+  getElem?_pmap ..
+
 @[simp]
 theorem getElem?_attach {xs : List α} {i : Nat} :
-    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) := by
-  induction xs generalizing i with
-  | nil => simp
-  | cons x xs ih =>
-    rcases i with ⟨i⟩
-    · simp only [attach_cons, Option.pmap]
-      split <;> simp_all
-    · simp only [attach_cons, getElem?_cons_succ, getElem?_map, ih]
-      simp only [Option.pmap]
-      split <;> split <;> simp_all
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) :=
+  getElem?_attachWith
+
+@[simp]
+theorem getElem_attachWith {xs : List α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
+    {i : Nat} (h : i < (xs.attachWith P H).length) :
+    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
+  getElem_pmap ..
 
 @[simp]
 theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
-    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem xs i (by simpa using h)⟩ := by
-  apply Option.some.inj
-  rw [← getElem?_eq_getElem]
-  rw [getElem?_attach]
-  simp only [Option.pmap]
-  split <;> rename_i h' _
-  · simp at h
-    simp at h'
-    exfalso
-    exact Nat.lt_irrefl _ (Nat.lt_of_le_of_lt h' h)
-  · simp only [Option.some.injEq, Subtype.mk.injEq]
-    apply Option.some.inj
-    rw [← getElem?_eq_getElem, h']
+    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
+  getElem_attachWith h
 
 @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs → P a) :
@@ -250,11 +290,23 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
   | nil => simp at h
   | cons x xs ih => simp [head_pmap, ih]
 
+@[simp] theorem head?_attachWith {P : α → Prop} {xs : List α}
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.attachWith P H).head? = xs.head?.pbind (fun a h => some ⟨a, H _ (mem_of_mem_head? h)⟩) := by
+  cases xs <;> simp_all
+
+@[simp] theorem head_attachWith {P : α → Prop} {xs : List α}
+    {H : ∀ (a : α), a ∈ xs → P a} (h : xs.attachWith P H ≠ []) :
+    (xs.attachWith P H).head h = ⟨xs.head (by simpa using h), H _ (head_mem _)⟩ := by
+  cases xs with
+  | nil => simp at h
+  | cons x xs => simp [head_attachWith, h]
+
 @[simp] theorem head?_attach (xs : List α) :
     xs.attach.head? = xs.head?.pbind (fun a h => some ⟨a, mem_of_mem_head? h⟩) := by
   cases xs <;> simp_all
 
-theorem head_attach {xs : List α} (h) :
+@[simp] theorem head_attach {xs : List α} (h) :
     xs.attach.head h = ⟨xs.head (by simpa using h), head_mem (by simpa using h)⟩ := by
   cases xs with
   | nil => simp at h
@@ -264,6 +316,32 @@ theorem attach_map {l : List α} (f : α → β) :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
   induction l <;> simp [*]
 
+theorem attachWith_map {l : List α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
+    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
+      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
+  induction l <;> simp [*]
+
+theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f =
+      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [attachWith_cons, map_cons, ih, pmap, cons.injEq, true_and]
+    apply pmap_congr_left
+    simp
+
+/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
+theorem map_attach {l : List α} (f : { x // x ∈ l } → β) :
+    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [attach_cons, map_cons, map_map, Function.comp_apply, pmap, cons.injEq, true_and, ih]
+    apply pmap_congr_left
+    simp
+
 theorem attach_filterMap {l : List α} {f : α → Option β} :
     (l.filterMap f).attach = l.attach.filterMap
       fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
@@ -304,6 +382,9 @@ theorem attach_filter {l : List α} (p : α → Bool) :
   ext1
   split <;> simp
 
+-- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
+-- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
       pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
@@ -334,6 +415,12 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ :
   congr 1 <;>
   exact pmap_congr_left _ fun _ _ _ _ => rfl
 
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α}
+    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
+    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_of_mem_left ys h)) ++
+      ys.attachWith P (fun a h => H a (mem_append_of_mem_right xs h)) := by
+  simp only [attachWith, attach_append, map_pmap, pmap_append]
+
 @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
@@ -344,6 +431,17 @@ theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : List α}
+    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
+    xs.reverse.attachWith P H =
+      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse :=
+  pmap_reverse ..
+
+theorem reverse_attachWith {P : α → Prop} {xs : List α}
+    {H : ∀ (a : α), a ∈ xs → P a} :
+    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) :=
+  reverse_pmap ..
+
 @[simp] theorem attach_reverse (xs : List α) :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
@@ -358,17 +456,6 @@ theorem reverse_attach (xs : List α) :
   intros
   rfl
 
-@[simp]
-theorem getLast?_attach {xs : List α} :
-    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast?_eq_some h⟩ := by
-  rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach]
-  simp
-
-@[simp]
-theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
-    xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩ := by
-  simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach]
-
 @[simp] theorem getLast?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).getLast? = xs.attach.getLast?.map fun ⟨a, m⟩ => f a (H a m) := by
@@ -383,4 +470,26 @@ theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
   simp only [getLast_eq_head_reverse]
   simp only [reverse_pmap, head_pmap, head_reverse]
 
+@[simp] theorem getLast?_attachWith {P : α → Prop} {xs : List α}
+    {H : ∀ (a : α), a ∈ xs → P a} :
+    (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast?_eq_some h)⟩) := by
+  rw [getLast?_eq_head?_reverse, reverse_attachWith, head?_attachWith]
+  simp
+
+@[simp] theorem getLast_attachWith {P : α → Prop} {xs : List α}
+    {H : ∀ (a : α), a ∈ xs → P a} (h : xs.attachWith P H ≠ []) :
+    (xs.attachWith P H).getLast h = ⟨xs.getLast (by simpa using h), H _ (getLast_mem _)⟩ := by
+  simp only [getLast_eq_head_reverse, reverse_attachWith, head_attachWith, head_map]
+
+@[simp]
+theorem getLast?_attach {xs : List α} :
+    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast?_eq_some h⟩ := by
+  rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach]
+  simp
+
+@[simp]
+theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
+    xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩ := by
+  simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach]
+
 end List

src/Init/Data/List/Basic.lean

@@ -1588,6 +1588,14 @@ such that adjacent elements are related by `R`.
   | []    => []
   | a::as => loop as a [] []
 where
+  /--
+  The arguments of `groupBy.loop l ag g gs` represent the following:
+
+  - `l : List α` are the elements which we still need to group.
+  - `ag : α` is the previous element for which a comparison was performed.
+  - `g : List α` is the group currently being assembled, in **reverse order**.
+  - `gs : List (List α)` is all of the groups that have been completed, in **reverse order**.
+  -/
   @[specialize] loop : List α → α → List α → List (List α) → List (List α)
   | a::as, ag, g, gs => match R ag a with
     | true  => loop as a (ag::g) gs

src/Init/Data/List/BasicAux.lean

@@ -155,7 +155,7 @@ def mapMono (as : List α) (f : α → α) : List α :=
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 
-theorem getElem_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by
+theorem getElem_append_left {as bs : List α} (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>
@@ -163,12 +163,14 @@ theorem getElem_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++
     | zero => rfl
     | succ i => apply ih
 
-theorem getElem_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs)[i]'h' = bs[i - as.length]'h'' := by
+theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂} :
+    (as ++ bs)[i]'h₂ =
+      bs[i - as.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) := by
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>
-    cases i with simp [get, Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h
-    | succ i => apply ih; simp [h]
+    cases i with simp [get, Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h₁
+    | succ i => apply ih; simp [h₁]
 
 theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
   cases i; rename_i i h'

src/Init/Data/List/Lemmas.lean

@@ -109,6 +109,9 @@ theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b
 theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
   | c :: l', _ => ⟨c, l', rfl⟩
 
+theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
+  simp
+
 /-! ### length -/
 
 theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
@@ -480,9 +483,9 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
-theorem getElem_mem : ∀ (l : List α) n (h : n < l.length), l[n]'h ∈ l
+theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
-  | _ :: l, _+1, _ => .tail _ (getElem_mem l ..)
+  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
 theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
   | _ :: _, 0, _ => .head ..
@@ -524,7 +527,7 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
       · simpa
       · apply w
         simp only [getElem_cons_succ]
-        exact getElem_mem l n (lt_of_succ_lt_succ h)
+        exact getElem_mem (lt_of_succ_lt_succ h)
 
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
@@ -729,6 +732,45 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
 
 -- See also `set_eq_take_append_cons_drop` in `Init.Data.List.TakeDrop`.
 
+/-! ### BEq -/
+
+@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (List α) ↔ ReflBEq α := by
+  constructor
+  · intro h
+    constructor
+    intro a
+    suffices ([a] == [a]) = true by
+      simpa only [List.instBEq, List.beq, Bool.and_true]
+    simp
+  · intro h
+    constructor
+    intro a
+    induction a with
+    | nil => simp only [List.instBEq, List.beq]
+    | cons a as ih =>
+      simp [List.instBEq, List.beq]
+      exact ih
+
+@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (List α) ↔ LawfulBEq α := by
+  constructor
+  · intro h
+    constructor
+    · intro a b h
+      apply singleton_inj.1
+      apply eq_of_beq
+      simp only [List.instBEq, List.beq]
+      simpa
+    · intro a
+      suffices ([a] == [a]) = true by
+        simpa only [List.instBEq, List.beq, Bool.and_true]
+      simp
+  · intro h
+    constructor
+    · intro a b h
+      simpa using h
+    · intro a
+      simp
+
 /-! ### Lexicographic ordering -/
 
 protected theorem lt_irrefl [LT α] (lt_irrefl : ∀ x : α, ¬x < x) (l : List α) : ¬l < l := by
@@ -929,6 +971,10 @@ theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
   | [_], _ => .head ..
   | _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
 
+theorem getLast_mem_getLast? : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ getLast? l
+  | [], h => by contradiction
+  | a :: l, _ => rfl
+
 theorem getLastD_mem_cons : ∀ (l : List α) (a : α), getLastD l a ∈ a::l
   | [], _ => .head ..
   | _::_, _ => .tail _ <| getLast_mem _
@@ -1026,6 +1072,10 @@ theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l
     cases h
     exact mem_cons_self a l
 
+theorem head_mem_head? : ∀ {l : List α} (h : l ≠ []), head l h ∈ head? l
+  | [], h => by contradiction
+  | a :: l, _ => rfl
+
 theorem head?_concat {a : α} : (l ++ [a]).head? = l.head?.getD a := by
   cases l <;> simp
 
@@ -1507,10 +1557,11 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 
 /-! ### append -/
 
-theorem getElem_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length),
-    (l₁ ++ l₂)[n]'(length_append .. ▸ Nat.lt_add_right _ h) = l₁[n]
-| a :: l, _, 0, h => rfl
-| a :: l, _, n+1, h => by simp only [get, cons_append]; apply getElem_append
+theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h) :
+    (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
+  split <;> rename_i h'
+  · rw [getElem_append_left h']
+  · rw [getElem_append_right (by simpa using h')]
 
 theorem getElem?_append_left {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
     (l₁ ++ l₂)[n]? = l₁[n]? := by
@@ -1536,12 +1587,13 @@ theorem get?_append_right {l₁ l₂ : List α} {n : Nat} (h : l₁.length ≤ n
     (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) := by
   simp [getElem?_append_right, h]
 
-theorem getElem_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) :
-    (l₁ ++ l₂)[n]'h₂ =
-      l₂[n - l₁.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) :=
-  Option.some.inj <| by rw [← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_append_right h₁]
+/-- Variant of `getElem_append_left` useful for rewriting from the small list to the big list. -/
+theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {n : Nat} (hn : n < l₁.length) :
+    l₁[n] = (l₁ ++ l₂)[n]'(by simpa using Nat.lt_add_right l₂.length hn) := by
+  rw [getElem_append_left] <;> simp
 
-theorem getElem_append_right'' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) :
+/-- Variant of `getElem_append_right` useful for rewriting from the small list to the big list. -/
+theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) :
     l₂[n] = (l₁ ++ l₂)[n + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hn _) := by
   rw [getElem_append_right] <;> simp [*, le_add_left]
 
@@ -1552,7 +1604,7 @@ theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat}
   exact Nat.sub_lt_left_of_lt_add h₁ h₂
 
 set_option linter.deprecated false in
-@[deprecated getElem_append_right' (since := "2024-06-12")]
+@[deprecated getElem_append_right (since := "2024-06-12")]
 theorem get_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) :
     (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, get_append_right_aux h₁ h₂⟩ :=
   Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]
@@ -1644,7 +1696,7 @@ theorem get_append_left (as bs : List α) (h : i < as.length) {h'} :
   simp [getElem_append_left, h, h']
 
 @[deprecated getElem_append_right (since := "2024-06-12")]
-theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} :
+theorem get_append_right (as bs : List α) (h : as.length ≤ i) {h' h''} :
     (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by
   simp [getElem_append_right, h, h', h'']
 
@@ -2323,6 +2375,47 @@ theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (rep
 @[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   cases n <;> simp [replicate_succ]
 
+/-- Every list is either empty, a non-empty `replicate`, or begins with a non-empty `replicate`
+followed by a different element. -/
+theorem eq_replicate_or_eq_replicate_append_cons {α : Type _} (l : List α) :
+    (l = []) ∨ (∃ n a, l = replicate n a ∧ 0 < n) ∨
+      (∃ n a b l', l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b) := by
+  induction l with
+  | nil => simp
+  | cons x l ih =>
+    right
+    rcases ih with rfl | ⟨n, a, rfl, h⟩ | ⟨n, a, b, l', rfl, h⟩
+    · left
+      exact ⟨1, x, rfl, by decide⟩
+    · by_cases h' : x = a
+      · subst h'
+        left
+        exact ⟨n + 1, x, rfl, by simp⟩
+      · right
+        refine ⟨1, x, a, replicate (n - 1) a, ?_, by decide, h'⟩
+        match n with | n + 1 => simp [replicate_succ]
+    · right
+      by_cases h' : x = a
+      · subst h'
+        refine ⟨n + 1, x, b, l', by simp [replicate_succ], by simp, h.2⟩
+      · refine ⟨1, x, a, replicate (n - 1) a ++ b :: l', ?_, by decide, h'⟩
+        match n with | n + 1 => simp [replicate_succ]
+
+/-- An induction principle for lists based on contiguous runs of identical elements. -/
+-- A `Sort _` valued version would require a different design. (And associated `@[simp]` lemmas.)
+theorem replicateRecOn {α : Type _} {p : List α → Prop} (m : List α)
+    (h0 : p []) (hr : ∀ a n, 0 < n → p (replicate n a))
+    (hi : ∀ a b n l, a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)) : p m := by
+  rcases eq_replicate_or_eq_replicate_append_cons m with
+    rfl | ⟨n, a, rfl, hn⟩ | ⟨n, a, b, l', w, hn, h⟩
+  · exact h0
+  · exact hr _ _ hn
+  · have : (b :: l').length < m.length := by
+      simpa [w] using Nat.lt_add_of_pos_left hn
+    subst w
+    exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
+termination_by m.length
+
 /-! ### reverse -/
 
 @[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by

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

@@ -176,7 +176,7 @@ theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) :=
 theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
   apply List.ext_getElem
   · simp
-  · simp (config := { contextual := true }) [← getElem_take, Nat.lt_min]
+  · simp (config := { contextual := true }) [getElem_take, Nat.lt_min]
 
 theorem nodup_range (n : Nat) : Nodup (range n) := by
   simp (config := {decide := true}) only [range_eq_range', nodup_range']

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

@@ -36,23 +36,23 @@ theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by sim
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the big list to the small list. -/
-theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+theorem getElem_take' (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
     L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) :=
-  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append ..
+  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append_left ..
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
-theorem getElem_take' (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
     (L.take j)[i] =
     L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
-  rw [length_take, Nat.lt_min] at h; rw [getElem_take L _ h.1]
+  rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the big list to the small list. -/
-@[deprecated getElem_take (since := "2024-06-12")]
+@[deprecated getElem_take' (since := "2024-06-12")]
 theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
     get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
-  simp [getElem_take _ hi hj]
+  simp [getElem_take' _ hi hj]
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
@@ -60,7 +60,7 @@ length `> i`. Version designed to rewrite from the small list to the big list. -
 theorem get_take' (L : List α) {j i} :
     get (L.take j) i =
     get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
-  simp [getElem_take']
+  simp [getElem_take]
 
 theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n)[m]? = none :=
@@ -110,7 +110,7 @@ theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none e
 
 theorem getLast_take {l : List α} (h : l.take n ≠ []) :
     (l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all)) := by
-  rw [getLast_eq_getElem, getElem_take']
+  rw [getLast_eq_getElem, getElem_take]
   simp [length_take, Nat.min_def]
   simp at h
   split
@@ -196,7 +196,7 @@ theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
 theorem take_prefix_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+: take n l := by
   rw [isPrefix_iff]
   intro i w
-  rw [getElem?_take_of_lt, getElem_take', getElem?_eq_getElem]
+  rw [getElem?_take_of_lt, getElem_take, getElem?_eq_getElem]
   simp only [length_take] at w
   exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le w (Nat.min_le_left _ _)) h
 
@@ -219,8 +219,9 @@ dropping the first `i` elements. Version designed to rewrite from the big list t
 theorem getElem_drop' (L : List α) {i j : Nat} (h : i + j < L.length) :
     L[i + j] = (L.drop i)[j]'(lt_length_drop L h) := by
   have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
-  rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right'] <;>
-    simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
+  rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right]
+  · simp [Nat.min_eq_left this, Nat.add_sub_cancel_left]
+  · simp [Nat.min_eq_left this, Nat.le_add_right]
 
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
@@ -267,9 +268,9 @@ theorem mem_take_iff_getElem {l : List α} {a : α} :
   constructor
   · rintro ⟨i, hm, rfl⟩
     simp at hm
-    refine ⟨i, by omega, by rw [getElem_take']⟩
+    refine ⟨i, by omega, by rw [getElem_take]⟩
   · rintro ⟨i, hm, rfl⟩
-    refine ⟨i, by simpa, by rw [getElem_take']⟩
+    refine ⟨i, by simpa, by rw [getElem_take]⟩
 
 theorem mem_drop_iff_getElem {l : List α} {a : α} :
     a ∈ l.drop n ↔ ∃ (i : Nat) (hm : i + n < l.length), l[n + i] = a := by
@@ -478,7 +479,7 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
     · simp only [take_succ_cons, findIdx?_cons]
       split
       · simp
-      · simp [ih, Option.guard_comp]
+      · simp [ih, Option.guard_comp, Option.bind_map]
 
 @[simp] theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
     min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a) := by

src/Init/Data/List/Sublist.lean

@@ -667,7 +667,7 @@ theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
 theorem IsPrefix.getElem {x y : List α} (h : x <+: y) {n} (hn : n < x.length) :
     x[n] = y[n]'(Nat.le_trans hn h.length_le) := by
   obtain ⟨_, rfl⟩ := h
-  exact (List.getElem_append n hn).symm
+  exact (List.getElem_append_left hn).symm
 
 -- See `Init.Data.List.Nat.Sublist` for `IsSuffix.getElem`.
 

src/Init/Data/Nat/Basic.lean

@@ -514,6 +514,10 @@ protected theorem add_lt_add_left {n m : Nat} (h : n < m) (k : Nat) : k + n < k
 protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m + k :=
   Nat.add_comm k m ▸ Nat.add_comm k n ▸ Nat.add_lt_add_left h k
 
+protected theorem lt_add_of_pos_left (h : 0 < k) : n < k + n := by
+  rw [Nat.add_comm]
+  exact Nat.add_lt_add_left h n
+
 protected theorem lt_add_of_pos_right (h : 0 < k) : n < n + k :=
   Nat.add_lt_add_left h n
 
@@ -718,7 +722,7 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
 
 theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
-instance {n : Nat} : NeZero (succ n) := ⟨succ_ne_zero n⟩
+instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩
 
 /-! # mul + order -/
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -226,12 +226,12 @@ private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
     simp [Nat.mod_eq (x+2) 2, p, hyp]
     cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]
 
-private theorem testBit_succ_zero : testBit (x + 1) 0 = not (testBit x 0) := by
+private theorem testBit_succ_zero : testBit (x + 1) 0 = !(testBit x 0) := by
   simp [testBit_to_div_mod, succ_mod_two]
   cases Nat.mod_two_eq_zero_or_one x with | _ p =>
     simp [p]
 
-theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = not (testBit x i) := by
+theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i) := by
   simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]
   cases mod_two_eq_zero_or_one (x / 2 ^ i) with
   | _ p => simp [p]

src/Init/Data/Nat/Lemmas.lean

@@ -84,9 +84,6 @@ protected theorem add_lt_add_of_lt_of_le {a b c d : Nat} (hlt : a < b) (hle : c
     a + c < b + d :=
   Nat.lt_of_le_of_lt (Nat.add_le_add_left hle _) (Nat.add_lt_add_right hlt _)
 
-protected theorem lt_add_of_pos_left : 0 < k → n < k + n := by
-  rw [Nat.add_comm]; exact Nat.lt_add_of_pos_right
-
 protected theorem pos_of_lt_add_right (h : n < n + k) : 0 < k :=
   Nat.lt_of_add_lt_add_left h
 

src/Init/Data/Option/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 prelude
 import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
+import Init.Data.BEq
 import Init.Classical
 import Init.Ext
 
@@ -247,7 +248,7 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
 theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
     x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
 
-@[simp] theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
+theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
     (x.map f).bind g = x.bind (g ∘ f) := by cases x <;> simp
 
 @[simp] theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :
@@ -411,6 +412,37 @@ variable [BEq α]
 @[simp] theorem some_beq_none (a : α) : ((some a : Option α) == none) = false := rfl
 @[simp] theorem some_beq_some {a b : α} : (some a == some b) = (a == b) := rfl
 
+@[simp] theorem reflBEq_iff : ReflBEq (Option α) ↔ ReflBEq α := by
+  constructor
+  · intro h
+    constructor
+    intro a
+    suffices (some a == some a) = true by
+      simpa only [some_beq_some]
+    simp
+  · intro h
+    constructor
+    · rintro (_ | a) <;> simp
+
+@[simp] theorem lawfulBEq_iff : LawfulBEq (Option α) ↔ LawfulBEq α := by
+  constructor
+  · intro h
+    constructor
+    · intro a b h
+      apply Option.some.inj
+      apply eq_of_beq
+      simpa
+    · intro a
+      suffices (some a == some a) = true by
+        simpa only [some_beq_some]
+      simp
+  · intro h
+    constructor
+    · intro a b h
+      simpa using h
+    · intro a
+      simp
+
 end beq
 
 /-! ### ite -/

src/Init/Data/UInt/Basic.lean

@@ -290,11 +290,17 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
+-- This instance would interfere with the global instance `NeZero (n + 1)`,
+-- so we only enable it locally.
+@[local instance]
+private def instNeZeroUSizeSize : NeZero USize.size := ⟨add_one_ne_zero _⟩
+
+@[deprecated (since := "2024-09-16")]
 theorem usize_size_gt_zero : USize.size > 0 :=
   Nat.zero_lt_succ ..
 
 @[extern "lean_usize_of_nat"]
-def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' n usize_size_gt_zero⟩
+def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat'  _ n⟩
 abbrev Nat.toUSize := USize.ofNat
 @[extern "lean_usize_to_nat"]
 def USize.toNat (n : USize) : Nat := n.val.val

src/Init/Prelude.lean

@@ -1014,7 +1014,7 @@ with `Or : Prop → Prop → Prop`, which is the propositional connective).
 It is `@[macro_inline]` because it has C-like short-circuiting behavior:
 if `x` is true then `y` is not evaluated.
 -/
-@[macro_inline] def or (x y : Bool) : Bool :=
+@[macro_inline] def Bool.or (x y : Bool) : Bool :=
   match x with
   | true  => true
   | false => y
@@ -1025,7 +1025,7 @@ with `And : Prop → Prop → Prop`, which is the propositional connective).
 It is `@[macro_inline]` because it has C-like short-circuiting behavior:
 if `x` is false then `y` is not evaluated.
 -/
-@[macro_inline] def and (x y : Bool) : Bool :=
+@[macro_inline] def Bool.and (x y : Bool) : Bool :=
   match x with
   | false => false
   | true  => y
@@ -1034,10 +1034,12 @@ if `x` is false then `y` is not evaluated.
 `not x`, or `!x`, is the boolean "not" operation (not to be confused
 with `Not : Prop → Prop`, which is the propositional connective).
 -/
-@[inline] def not : Bool → Bool
+@[inline] def Bool.not : Bool → Bool
   | true  => false
   | false => true
 
+export Bool (or and not)
+
 /--
 The type of natural numbers, starting at zero. It is defined as an
 inductive type freely generated by "zero is a natural number" and

src/Lean/Compiler/IR/RC.lean

@@ -91,7 +91,7 @@ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Na
     | Arg.var y      => x == y && !consumeParamPred i
 
 private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool :=
-  isBorrowParamAux x ys fun i => not ps[i]!.borrow
+  isBorrowParamAux x ys fun i => ! ps[i]!.borrow
 
 /--
 Return `n`, the number of times `x` is consumed.
@@ -124,7 +124,7 @@ private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred :
         addInc ctx x b numIncs
 
 private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
-  addIncBeforeAux ctx xs (fun i => not ps[i]!.borrow) b liveVarsAfter
+  addIncBeforeAux ctx xs (fun i => ! ps[i]!.borrow) b liveVarsAfter
 
 /-- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application.  -/
 private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=

src/Lean/Data/PersistentArray.lean

@@ -317,8 +317,8 @@ variable {m : Type → Type w} [Monad m]
   anyMAux p t.root <||> t.tail.anyM p
 
 @[inline] def allM (a : PersistentArray α) (p : α → m Bool) : m Bool := do
-  let b ← anyM a (fun v => do let b ← p v; pure (not b))
-  pure (not b)
+  let b ← anyM a (fun v => do let b ← p v; pure (!b))
+  pure (!b)
 
 end
 

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

@@ -599,7 +599,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
             all_le := false
             break
       -- No progress here? Try the next measure
-      if not (has_lt && all_le) then continue
+      if !(has_lt && all_le) then continue
       -- We found a suitable measure, remove it from the list (mild optimization)
       let measures' := measures.eraseIdx measureIdx
       return ← go measures' todo (acc.push measure)

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

@@ -56,7 +56,7 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
     let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
     let proof := return mkRefl (mkConst ``Bool.false)
     return some ⟨boolExpr, proof, expr⟩
-  | not subExpr =>
+  | Bool.not subExpr =>
     let some sub ← of subExpr | return none
     let boolExpr := .not sub.bvExpr
     let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
@@ -65,9 +65,9 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
       let subProof ← sub.evalsAtAtoms
       return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
     return some ⟨boolExpr, proof, expr⟩
-  | or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
-  | and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
-  | xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
+  | Bool.or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
+  | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
+  | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
   | BEq.beq α _ lhsExpr rhsExpr =>
     match_expr α with
     | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr

src/Lean/Elab/Term.lean

@@ -1439,7 +1439,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
     let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
       let localDecl ← localDecl?
       if localDecl.isAuxDecl then
-        guard (not skipAuxDecl)
+        guard (!skipAuxDecl)
         if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
           matchAuxRecDecl? localDecl fullDeclName givenNameView
         else
@@ -1497,7 +1497,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
       foo := 10
     ```
     -/
-    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && not projs.isEmpty) with
+    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && !projs.isEmpty) with
     | some decl => return some (decl.toExpr, projs)
     | none => match n with
       | .str pre s => loop pre (s::projs) globalDeclFoundNext

src/Lean/Meta/Check.lean

@@ -82,7 +82,7 @@ where
         return (a, b)
       else if a.getAppNumArgs != b.getAppNumArgs then
         return (a, b)
-      else if not (← isDefEq a.getAppFn b.getAppFn) then
+      else if !(← isDefEq a.getAppFn b.getAppFn) then
         return (a, b)
       else
         let fType ← inferType a.getAppFn

src/Lean/Meta/DiscrTree.lean

@@ -211,7 +211,7 @@ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Boo
     if info.isInstImplicit then
       return true
     else if info.isImplicit || info.isStrictImplicit then
-      return not (← isType a)
+      return !(← isType a)
     else
       isProof a
   else

src/Lean/Meta/ExprDefEq.lean

@@ -418,7 +418,7 @@ This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that
 where the index is the position in the local context.
 -/
 private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do
-  if not (← hasLetDeclsInBetween) then
+  if !(← hasLetDeclsInBetween) then
     mkLambdaFVars xs v (etaReduce := true)
   else
     let ys ← addLetDeps

src/Lean/Meta/LazyDiscrTree.lean

@@ -77,7 +77,7 @@ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Boo
     if info.isInstImplicit then
       return true
     else if info.isImplicit || info.isStrictImplicit then
-      return not (← isType a)
+      return !(← isType a)
     else
       isProof a
   else

src/Lean/Meta/Tactic/FunInd.lean

@@ -438,9 +438,11 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
   let mvar ← mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp)
   let mut mvarId := mvar.mvarId!
   mvarId ← assertIHs IHs mvarId
+  trace[Meta.FunInd] "Goal before cleanup:{mvarId}"
   for fvarId in toClear do
     mvarId ← mvarId.clear fvarId
   mvarId ← mvarId.cleanup (toPreserve := toPreserve)
+  trace[Meta.FunInd] "Goal after cleanup (toClear := {toClear.map mkFVar}) (toPreserve := {toPreserve.map mkFVar}):{mvarId}"
   modify (·.push mvarId)
   let mvar ← instantiateMVars mvar
   pure mvar

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

@@ -77,8 +77,9 @@ builtin_dsimproc [simp, seval] reduceFinMk (Fin.mk _ _)  := fun e => do
   let_expr Fin.mk n v _ ← e | return .continue
   let some n ← evalNat n |>.run | return .continue
   let some v ← getNatValue? v | return .continue
-  if h : n > 0 then
-    return .done <| toExpr (Fin.ofNat' v h)
+  if h : n ≠ 0 then
+    have : NeZero n := ⟨h⟩
+    return .done <| toExpr (Fin.ofNat' n v)
   else
     return .continue
 

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -137,7 +137,7 @@ def isNonConstFun (motive : Expr) : MetaM Bool := do
   | _ => return motive.hasLooseBVars
 
 def isSimpleHOFun (motive : Expr) : MetaM Bool :=
-  return not (← returnsPi motive) && not (← isNonConstFun motive)
+  return !(← returnsPi motive) && !(← isNonConstFun motive)
 
 def isType2Type (motive : Expr) : MetaM Bool := do
   match ← inferType motive with
@@ -278,7 +278,7 @@ where
   inspectAux (fType mType : Expr) (i : Nat) (args mvars : Array Expr) := do
     let fType ← whnf fType
     let mType ← whnf mType
-    if not (i < args.size) then return ()
+    if !(i < args.size) then return ()
     match fType, mType with
     | Expr.forallE _ fd fb _, Expr.forallE _ _  mb _ => do
       -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here?
@@ -324,7 +324,7 @@ def withKnowing (knowsType knowsLevel : Bool) (x : AnalyzeM α) : AnalyzeM α :=
 builtin_initialize analyzeFailureId : InternalExceptionId ← registerInternalExceptionId `analyzeFailure
 
 def checkKnowsType : AnalyzeM Unit := do
-  if not (← read).knowsType then
+  if !(← read).knowsType then
     throw $ Exception.internal analyzeFailureId
 
 def annotateBoolAt (n : Name) (pos : Pos) : AnalyzeM Unit := do
@@ -425,7 +425,7 @@ mutual
         funBinders   := mkArray args.size false
       }
 
-      if not rest.isEmpty then
+      if !rest.isEmpty then
         -- Note: this shouldn't happen for type-correct terms
         if !args.isEmpty then
           analyzeAppStaged (mkAppN f args) rest
@@ -501,11 +501,11 @@ mutual
     collectHigherOrders := do
       let { args, mvars, bInfos, ..} ← read
       for i in [:args.size] do
-        if not (bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
-        if not (← isHigherOrder (← inferType args[i]!)) then continue
+        if !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
+        if !(← isHigherOrder (← inferType args[i]!)) then continue
         if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue
 
-        if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && not (← valUnknown mvars[i]!)
+        if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && !(← valUnknown mvars[i]!)
           && (← isType2Type (args[i]!)) && (← isFOLike (args[i]!)) then continue
 
         tryUnify args[i]! mvars[i]!
@@ -602,7 +602,7 @@ mutual
               | _                 => annotateNamedArg (← mvarName mvars[i]!)
             else annotateBool `pp.analysis.skip; provided := false
             modify fun s => { s with provideds := s.provideds.set! i provided }
-          if (← get).provideds[i]! then withKnowing (not (← typeUnknown mvars[i]!)) true analyze
+          if (← get).provideds[i]! then withKnowing (!(← typeUnknown mvars[i]!)) true analyze
           tryUnify mvars[i]! args[i]!
 
     maybeSetExplicit := do

src/Std/Data/DHashMap/Basic.lean

@@ -260,6 +260,10 @@ 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/Internal/Model.lean

@@ -98,14 +98,14 @@ theorem exists_bucket_of_uset [BEq α] [Hashable α]
     refine ⟨?_, ?_⟩
     · apply List.containsKey_bind_eq_false
       intro j hj
-      rw [← List.getElem_append (l₂ := self[i] :: l₂), getElem_congr_coll h₁.symm]
+      rw [List.getElem_append_left' (l₂ := self[i] :: l₂), getElem_congr_coll h₁.symm]
       apply (h.hashes_to j _).containsKey_eq_false h₀ k
       omega
     · apply List.containsKey_bind_eq_false
       intro j hj
       rw [← List.getElem_cons_succ self[i] _ _
         (by simp only [Array.ugetElem_eq_getElem, List.length_cons]; omega)]
-      rw [List.getElem_append_right'' l₁, getElem_congr_coll h₁.symm]
+      rw [List.getElem_append_right' l₁, getElem_congr_coll h₁.symm]
       apply (h.hashes_to (j + 1 + l₁.length) _).containsKey_eq_false h₀ k
       omega
 

src/Std/Data/DHashMap/Raw.lean

@@ -411,6 +411,14 @@ 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

@@ -250,6 +250,10 @@ 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

@@ -212,6 +212,14 @@ 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/Sat/CNF/Literal.lean

@@ -21,7 +21,7 @@ namespace Literal
 /--
 Flip the polarity of `l`.
 -/
-def negate (l : Literal α) : Literal α := (l.1, not l.2)
+def negate (l : Literal α) : Literal α := (l.1, !l.2)
 
 end Literal
 

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

@@ -37,15 +37,11 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
 theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderCarry aig input, assign⟧
       =
-    or
-      (and
-        (xor
+      ((xor
           ⟦aig, input.lhs, assign⟧
-          ⟦aig, input.rhs, assign⟧)
-        ⟦aig, input.cin, assign⟧)
-      (and
-        ⟦aig, input.lhs, assign⟧
-        ⟦aig, input.rhs, assign⟧)
+          ⟦aig, input.rhs, assign⟧) &&
+        ⟦aig, input.cin, assign⟧ ||
+       ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)
     := by
   simp only [mkFullAdderCarry, Ref.cast_eq, Int.reduceNeg, denote_mkOrCached,
     LawfulOperator.denote_input_entry, denote_mkAndCached, denote_projected_entry',

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

@@ -33,7 +33,7 @@ def toString : Gate → String
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | or => (· || ·)
-  | xor => _root_.xor
+  | xor => Bool.xor
   | beq => (· == ·)
   | imp => (!· || ·)
 

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

@@ -21,12 +21,11 @@ theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Litera
   simp only [Literal.negate, sat_iff]
   constructor
   · intro h pl
-    rw [sat_iff, h, not.eq_def] at pl
-    split at pl <;> simp_all
+    rw [sat_iff, h] at pl
+    simp at pl
   · intro h
     rw [sat_iff] at h
-    rw [not.eq_def]
-    split <;> simp_all
+    cases h : p l.fst <;> simp_all
 
 theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) :
     Limplies α x l → Limplies α x (Literal.negate l) → Unsatisfiable α x := by

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

@@ -168,7 +168,7 @@ Attempts to add the literal `(idx, b)` to clause `c`. Returns none if doing so w
 tautology.
 -/
 def insert (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClause n) :=
-  if heq1 : c.clause.contains (l.1, not l.2) then
+  if heq1 : c.clause.contains (l.1, !l.2) then
     none -- Adding l would make c a tautology
   else if heq2 : c.clause.contains l then
     some c
@@ -353,7 +353,7 @@ def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin
         else
           .reducedToEmpty
       | .neg =>
-        if not l.2 then
+        if !l.2 then
           .reducedToUnit l
         else
           .reducedToEmpty
@@ -367,7 +367,7 @@ def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin
         else
           .reducedToUnit l'
       | .neg =>
-        if not l.2 then
+        if !l.2 then
           .reducedToNonunit -- Assignment fails to refute both l and l'
         else
           .reducedToUnit l'

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

@@ -219,7 +219,7 @@ def performRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHin
     let (f, derivedLits, derivedEmpty, encounteredError) := performRupCheck f rupHints
     if encounteredError then
       (f, false)
-    else if not derivedEmpty then
+    else if !derivedEmpty then
       (f, false)
     else -- derivedEmpty is true and encounteredError is false
       let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
@@ -284,7 +284,7 @@ def performRatCheck {n : Nat} (f : DefaultFormula n) (negPivot : Literal (PosFin
           -- assignments should now be the same as it was before the performRupCheck call
           let f := clearRatUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
           -- f should now be the same as it was before insertRatUnits
-          if encounteredError || not derivedEmpty then (f, false)
+          if encounteredError || !derivedEmpty then (f, false)
           else (f, true)
     | none => (⟨clauses, rupUnits, ratUnits, assignments⟩, false)
 
@@ -309,7 +309,7 @@ def performRatAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
           if allChecksPassed then performRatCheck f (Literal.negate pivot) ratHint
           else (f, false)
         let (f, allChecksPassed) := ratHints.foldl fold_fn (f, true)
-        if not allChecksPassed then (f, false)
+        if !allChecksPassed then (f, false)
         else
           match f with
           | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>

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

@@ -507,8 +507,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
-              simp only [← heq, not] at l_ne_b
-              split at l_ne_b <;> simp at l_ne_b
+              simp only [← heq] at l_ne_b
+              simp at l_ne_b
             · next id_ne_idx => simp [id_ne_idx]
           · exact hf
         · exact Or.inr hf

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

@@ -57,8 +57,8 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
     · split
       · next heq =>
-        simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
-        split at negl_ne_v <;> simp_all
+        simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
+        simp_all
       · next hne =>
         exact pv
   · exists v
@@ -67,8 +67,8 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
     · split
       · next heq =>
-        simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
-        split at negl_ne_v <;> simp_all
+        simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
+        simp_all
       · next hne =>
         exact pv
 

src/Std/Tactic/BVDecide/Reflect.lean

@@ -126,7 +126,7 @@ theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
   simp[*]
 
 theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (xor lhs' rhs') = (xor lhs rhs) := by
+    (Bool.xor lhs' rhs') = (xor lhs rhs) := by
   simp[*]
 
 theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :