feat: List.replicate lemmas

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₁ := hle) (h₂ := h')]
+  conv => rhs; rw [← List.getElem_append_right (h' := h') (h := Nat.not_lt_of_ge hle)]
   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' (2^n) i
+  toFin := Fin.ofNat' i (Nat.two_pow_pos n)
 
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
@@ -173,10 +173,6 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
 theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
   x[i] = x.toNat.testBit i := rfl
 
-theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
-    x.getLsbD i = x[i] := by
-  simp [getLsbD, getElem_eq_testBit_toNat]
-
 end getElem
 
 section Int

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' (2^w) x := rfl
+@[simp] theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat' x (Nat.two_pow_pos w) := 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.
@@ -273,30 +273,8 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
-@[simp] theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
-  simp [getElem_eq_testBit_toNat]
-
-@[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
-  simp [getElem_eq_testBit_toNat, h]
-
-@[simp] theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
-  simp [getElem?_eq_getElem]
-
-@[simp] theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
-  simp [getElem?_eq_getElem]
-
-@[simp] theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp [ofBool, cond_eq_if]
-  split <;> simp_all
-
-@[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
-  rw [getElem_eq_iff, getElem?_zero_ofBool]
-
-@[simp] theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
-  simp [ofBool]
-
 @[simp]
-theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && b) := by
+theorem getLsbD_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsbD i = ((i = 0) && b) := by
   rcases b with rfl | rfl
   · simp [ofBool]
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
@@ -352,10 +330,6 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 
 @[simp] theorem getMsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getMsbD i = x.getMsbD i := by
   subst h; simp
-
-@[simp] theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (cast h x)[i] = x[i] := by
-  subst h; simp
-
 @[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
   simp [BitVec.msb]
 
@@ -549,15 +523,6 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
   all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
-@[simp]
-theorem getElem_truncate (m : Nat) (x : BitVec n) (i : Nat) (hi : i < m) :
-    (truncate m x)[i] = x.getLsbD i := by
-  simp only [getElem_zeroExtend]
-
-theorem getElem?_truncate (m : Nat) (x : BitVec n) (i : Nat) :
-    (truncate m x)[i]? = if i < m then some (x.getLsbD i) else none :=
-  getElem?_zeroExtend m x i
-
 theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
   getLsbD_zeroExtend m x i
@@ -581,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 := x) (i := i)
+  have p := lt_of_getLsbD x i
   revert p
   cases getLsbD x i <;> simp; omega
 
@@ -627,12 +592,6 @@ 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]
@@ -674,9 +633,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 @[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
   simp [allOnes]
 
-@[simp] theorem getElem_allOnes (i : Nat) (h : i < v) : (allOnes v)[i] = true := by
-  simp [getElem_eq_testBit_toNat, h]
-
 @[simp] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by
   ext
   simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_True]
@@ -704,9 +660,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_or {x y : BitVec w} {i : Nat} (h : i < w) : (x ||| y)[i] = (x[i] || y[i]) := by
-  simp [getElem_eq_testBit_toNat]
-
 @[simp] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by
   simp [BitVec.msb]
 
@@ -745,9 +698,6 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_com
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_and {x y : BitVec w} {i : Nat} (h : i < w) : (x &&& y)[i] = (x[i] && y[i]) := by
-  simp [getElem_eq_testBit_toNat]
-
 @[simp] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by
   simp [BitVec.msb]
 
@@ -788,9 +738,6 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (xor x[i] y[i]) := by
-  simp [getElem_eq_testBit_toNat]
-
 @[simp] theorem msb_xor {x y : BitVec w} :
     (x ^^^ y).msb = (xor x.msb y.msb) := by
   simp [BitVec.msb]
@@ -844,12 +791,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 @[simp] theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i) := by
   by_cases h' : i < v <;> simp_all [not_def]
 
-@[simp] theorem getElem_not {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i] := by
-  simp only [getElem_eq_testBit_toNat, toNat_not]
-  rw [← Nat.sub_add_eq, Nat.add_comm 1]
-  rw [Nat.testBit_two_pow_sub_succ x.isLt]
-  simp [h]
-
 @[simp] theorem truncate_not {x : BitVec w} (h : k ≤ w) :
     (~~~x).truncate k = ~~~(x.truncate k) := by
   ext
@@ -885,7 +826,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' (2^w) (x.toNat <<< n) := rfl
+    BitVec.toFin (x <<< n) = Fin.ofNat' (x.toNat <<< n) (Nat.two_pow_pos w) := rfl
 
 @[simp]
 theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
@@ -1006,10 +947,6 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
     getLsbD (x >>> i) j = getLsbD x (i+j) := by
   unfold getLsbD ; simp
 
-@[simp] theorem getElem_ushiftRight (x : BitVec w) (i n : Nat) (h : i < w) :
-    (x >>> n)[i] = x.getLsbD (n + i) := by
-  simp [getElem_eq_testBit_toNat, toNat_ushiftRight, Nat.testBit_shiftRight, getLsbD]
-
 theorem ushiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) >>> n = (x >>> n) ^^^ (y >>> n) := by
   ext
@@ -1090,7 +1027,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,
@@ -1291,7 +1228,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
@@ -1322,18 +1259,6 @@ 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]
 
@@ -1583,7 +1508,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) (2^n - x.toNat) :=
+    (-x).toFin = Fin.ofNat' (2^n - x.toNat) (Nat.two_pow_pos _) :=
   rfl
 
 theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by

src/Init/Data/Bool.lean

@@ -6,11 +6,16 @@ Authors: F. G. Dorais
 prelude
 import Init.NotationExtra
 
+/-- Boolean exclusive or -/
+abbrev xor : Bool → Bool → Bool := bne
 
 namespace Bool
 
-/-- Boolean exclusive or -/
-abbrev xor : Bool → Bool → Bool := bne
+/- 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
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
@@ -592,7 +597,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
 
 end Bool
 
-export Bool (cond_eq_if xor and or not)
+export Bool (cond_eq_if)
 
 /-! ### 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 + 1)
+def succ : Fin n → Fin n.succ
   | ⟨i, h⟩ => ⟨i+1, Nat.succ_lt_succ h⟩
 
 variable {n : Nat}
@@ -39,20 +39,16 @@ variable {n : Nat}
 /--
 Returns `a` modulo `n + 1` as a `Fin n.succ`.
 -/
-protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
+protected def ofNat {n : Nat} (a : Nat) : Fin n.succ :=
   ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
 
 /--
 Returns `a` modulo `n` as a `Fin n`.
 
-The assumption `NeZero n` ensures that `Fin n` is nonempty.
+The assumption `n > 0` ensures that `Fin n` is nonempty.
 -/
-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
+protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
+  ⟨a % n, Nat.mod_lt _ h⟩
 
 private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
   | 0,   h => Nat.mod_lt _ h
@@ -145,10 +141,10 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin n) i where
-  ofNat := Fin.ofNat' n i
+instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin (no_index n)) i where
+  ofNat := Fin.ofNat' i (pos_of_neZero _)
 
-instance instInhabited {n : Nat} [NeZero n] : Inhabited (Fin n) where
+instance : Inhabited (Fin (no_index (n+1))) 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' (n : Nat) [NeZero n] (a : Nat) :
-  (Fin.ofNat' n a).val = a % n := rfl
+@[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
+  (Fin.ofNat' a is_pos).val = a % n := rfl
 
-@[simp] theorem ofNat'_val_eq_self [NeZero n](x : Fin n) : (Fin.ofNat' n x) = x := by
+@[simp] theorem ofNat'_val_eq_self (x : Fin n) (h) : (Fin.ofNat' x h) = 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 [NeZero n] (x : Nat) (y : Fin n) :
-    Fin.ofNat' n x + y = Fin.ofNat' n (x + y.val) := by
+@[simp] theorem ofNat'_add (x : Nat) (lt : 0 < n) (y : Fin n) :
+    Fin.ofNat' x lt + y = Fin.ofNat' (x + y.val) lt := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.add_def]
 
-@[simp] theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
-    x + Fin.ofNat' n y = Fin.ofNat' n (x.val + y) := by
+@[simp] theorem add_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
+    x + Fin.ofNat' y lt = Fin.ofNat' (x.val + y) lt := 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 [NeZero n] (x : Nat) (y : Fin n) :
-    Fin.ofNat' n x - y = Fin.ofNat' n ((n - y.val) + x) := by
+@[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
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
-@[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
+@[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
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 

src/Init/Data/List/Attach.lean

@@ -48,8 +48,6 @@ 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
@@ -83,12 +81,7 @@ theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
   subst h
   simp
 
-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 α} :
+@[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]
@@ -96,12 +89,6 @@ theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Pro
   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
@@ -117,18 +104,14 @@ 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 _ _ _
+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]
 
 @[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 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 mem_attach (l : List α) : ∀ x, x ∈ l.attach
@@ -154,11 +137,7 @@ 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 :=
-  length_pmap
-
-@[simp]
-theorem length_attachWith {p : α → Prop} {l H} : length (l.attachWith p H) = length l :=
+theorem length_attach (L : List α) : L.attach.length = L.length :=
   length_pmap
 
 @[simp]
@@ -176,15 +155,6 @@ 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
@@ -217,7 +187,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 (@length_pmap _ _ p f l h ▸ hn))) := by
+        (h _ (getElem_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
   induction l generalizing n with
   | nil =>
     simp only [length, pmap] at hn
@@ -235,26 +205,34 @@ 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) :=
-  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 ..
+    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
 
 @[simp]
 theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
-    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
-  getElem_attachWith h
+    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']
 
 @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs → P a) :
@@ -272,72 +250,20 @@ 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
 
-@[simp] theorem head_attach {xs : List α} (h) :
+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
   | cons x xs => simp [head_attach, h]
 
-@[simp] theorem tail_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
-    (H : ∀ (a : α), a ∈ xs → P a) :
-    (xs.pmap f H).tail = xs.tail.pmap f (fun a h => H a (mem_of_mem_tail h)) := by
-  cases xs <;> simp
-
-@[simp] theorem tail_attachWith {P : α → Prop} {xs : List α}
-    {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).tail = xs.tail.attachWith P (fun a h => H a (mem_of_mem_tail h)) := by
-  cases xs <;> simp
-
-@[simp] theorem tail_attach (xs : List α) :
-    xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
-  cases xs <;> simp
-
 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
@@ -378,9 +304,6 @@ 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
@@ -411,12 +334,6 @@ 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
@@ -427,17 +344,6 @@ 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]
@@ -452,6 +358,17 @@ 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
@@ -466,46 +383,4 @@ theorem reverse_attach (xs : List α) :
   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]
-
-@[simp]
-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]
-
-@[simp]
-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 _ _ _
-
 end List

src/Init/Data/List/Basic.lean

@@ -1588,14 +1588,6 @@ 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,14 +163,12 @@ 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 α} {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
+theorem getElem_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs)[i]'h' = bs[i - as.length]'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/Count.lean

@@ -115,13 +115,6 @@ theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂
 theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _
 theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _
 
--- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
-
-theorem countP_tail_le (l) : countP p l.tail ≤ countP p l :=
-  (tail_sublist l).countP_le _
-
--- See `Init.Data.List.Nat.Count` for `le_countP_tail : countP p l - 1 ≤ countP p l.tail`.
-
 theorem countP_filter (l : List α) :
     countP p (filter q l) = countP (fun a => p a && q a) l := by
   simp only [countP_eq_length_filter, filter_filter]
@@ -214,13 +207,6 @@ theorem IsPrefix.count_le (h : l₁ <+: l₂) (a : α) : count a l₁ ≤ count
 theorem IsSuffix.count_le (h : l₁ <:+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.sublist.count_le _
 theorem IsInfix.count_le (h : l₁ <:+: l₂) (a : α) : count a l₁ ≤ count a l₂ := h.sublist.count_le _
 
--- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`.
-
-theorem count_tail_le (a : α) (l) : count a l.tail ≤ count a l :=
-  (tail_sublist l).count_le _
-
--- See `Init.Data.List.Nat.Count` for `le_count_tail : count a l - 1 ≤ count a l.tail`.
-
 theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) :=
   (sublist_cons_self _ _).count_le _
 

src/Init/Data/List/Lemmas.lean

@@ -109,9 +109,6 @@ 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
@@ -483,9 +480,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) ..)
+  | _ :: l, _+1, _ => .tail _ (getElem_mem l ..)
 
 theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
   | _ :: _, 0, _ => .head ..
@@ -527,7 +524,7 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
       · simpa
       · apply w
         simp only [getElem_cons_succ]
-        exact getElem_mem (lt_of_succ_lt_succ h)
+        exact getElem_mem l n (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
@@ -732,45 +729,6 @@ 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
@@ -971,10 +929,6 @@ 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 _
@@ -1045,11 +999,6 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]?
   | [] => rfl
   | a :: l => by simp
 
-theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos.mpr h) := by
-  cases l with
-  | nil => simp at h
-  | cons _ _ => simp
-
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h
@@ -1077,10 +1026,6 @@ 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
 
@@ -1110,55 +1055,6 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
 theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l := by
   induction l <;> simp_all
 
-theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail ≠ [] → l ≠ [] := by
-  cases l <;> simp
-
-@[simp] theorem getElem_tail (l : List α) (i : Nat) (h : i < l.tail.length) :
-    (tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h)) := by
-  cases l with
-  | nil => simp at h
-  | cons _ l => simp
-
-@[simp] theorem getElem?_tail (l : List α) (i : Nat) :
-    (tail l)[i]? = l[i + 1]? := by
-  cases l <;> simp
-
-@[simp] theorem set_tail (l : List α) (i : Nat) (a : α) :
-    l.tail.set i a = (l.set (i + 1) a).tail := by
-  cases l <;> simp
-
-theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.length := by
-  cases l with
-  | nil => simp at h
-  | cons _ l =>
-    simp only [tail_cons, ne_eq] at h
-    exact Nat.lt_add_of_pos_left (length_pos.mpr h)
-
-@[simp] theorem head_tail (l : List α) (h : l.tail ≠ []) :
-    (tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h) := by
-  cases l with
-  | nil => simp at h
-  | cons _ l => simp [head_eq_getElem]
-
-@[simp] theorem head?_tail (l : List α) : (tail l).head? = l[1]? := by
-  simp [head?_eq_getElem?]
-
-@[simp] theorem getLast_tail (l : List α) (h : l.tail ≠ []) :
-    (tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h) := by
-  simp only [getLast_eq_getElem, length_tail, getElem_tail]
-  congr
-  match l with
-  | _ :: _ :: l => simp
-
-theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then none else l.getLast? := by
-  match l with
-  | [] => simp
-  | [a] => simp
-  | _ :: _ :: l =>
-    simp only [tail_cons, length_cons, getLast?_cons_cons]
-    rw [if_neg]
-    rintro ⟨⟩
-
 /-! ## Basic operations -/
 
 /-! ### map -/
@@ -1611,11 +1507,10 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 
 /-! ### 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 : ∀ {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_left {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
     (l₁ ++ l₂)[n]? = l₁[n]? := by
@@ -1641,13 +1536,12 @@ 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]
 
-/-- 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₁ 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_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) :
+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]
 
@@ -1658,7 +1552,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₁]
@@ -1750,7 +1644,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 : as.length ≤ i) {h' h''} :
+theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} :
     (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by
   simp [getElem_append_right, h, h', h'']
 
@@ -2901,12 +2795,6 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (
     dropLast (a :: replicate n a) = replicate n a := by
   rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel]
 
-@[simp] theorem tail_reverse (l : List α) : l.reverse.tail = l.dropLast.reverse := by
-  apply ext_getElem
-  · simp
-  · intro i h₁ h₂
-    simp [Nat.add_comm i, Nat.sub_add_eq]
-
 /-!
 ### splitAt
 

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

@@ -18,26 +18,6 @@ open Nat
 
 namespace List
 
-/-! ### dropLast -/
-
-theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := by
-  ext1
-  simp only [getElem?_tail, getElem?_dropLast, length_tail]
-  split <;> split
-  · rfl
-  · omega
-  · omega
-  · rfl
-
-@[simp] theorem dropLast_reverse (l : List α) : l.reverse.dropLast = l.tail.reverse := by
-  apply ext_getElem
-  · simp
-  · intro i h₁ h₂
-    simp only [getElem_dropLast, getElem_reverse, length_tail, getElem_tail]
-    congr
-    simp only [length_dropLast, length_reverse, length_tail] at h₁ h₂
-    omega
-
 /-! ### filter -/
 
 theorem length_filter_lt_length_iff_exists {l} :

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

@@ -28,59 +28,4 @@ theorem count_set [BEq α] (a b : α) (l : List α) (i : Nat) (h : i < l.length)
     (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
   simp [count_eq_countP, countP_set, h]
 
-/--
-The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list,
-minus the difference in the lengths.
--/
-theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ := by
-  match s with
-  | .slnil => simp
-  | .cons a s =>
-    rename_i l
-    simp only [countP_cons, length_cons]
-    have := s.le_countP p
-    have := s.length_le
-    split <;> omega
-  | .cons₂ a s =>
-    rename_i l₁ l₂
-    simp only [countP_cons, length_cons]
-    have := s.le_countP p
-    have := s.length_le
-    split <;> omega
-
-theorem IsPrefix.le_countP (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
-  s.sublist.le_countP _
-
-theorem IsSuffix.le_countP (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
-  s.sublist.le_countP _
-
-theorem IsInfix.le_countP (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
-  s.sublist.le_countP _
-
-/--
-The number of elements satisfying a predicate in the tail of a list is
-at least one less than the number of elements satisfying the predicate in the list.
--/
-theorem le_countP_tail (l) : countP p l - 1 ≤ countP p l.tail := by
-  have := (tail_sublist l).le_countP p
-  simp only [length_tail] at this
-  omega
-
-variable [BEq α]
-
-theorem Sublist.le_count (s : l₁ <+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.le_countP _
-
-theorem IsPrefix.le_count (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.sublist.le_count _
-
-theorem IsSuffix.le_count (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.sublist.le_count _
-
-theorem IsInfix.le_count (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
-  s.sublist.le_count _
-
-theorem le_count_tail (a : α) (l) : count a l - 1 ≤ count a l.tail :=
-  le_countP_tail _
-
 end List

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']
@@ -258,9 +258,6 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
   | zero => simp at h
   | succ n => simp
 
-@[simp] theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by
-  cases n <;> simp
-
 @[simp] theorem reverse_iota : reverse (iota n) = range' 1 n := by
   induction n with
   | zero => simp
@@ -451,9 +448,6 @@ theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
     l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by
   simp [getLast?_eq_getElem?]
 
-@[simp] theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by
-  simp [enum]
-
 theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x := by
   simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]
 

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_left ..
+  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append ..
 
 /-- 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,9 +219,8 @@ 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]
-  · simp [Nat.min_eq_left this, 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, 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. -/
@@ -268,9 +267,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
@@ -479,7 +478,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, Option.bind_map]
+      · simp [ih, Option.guard_comp]
 
 @[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/Range.lean

@@ -35,16 +35,11 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step)
 theorem range'_ne_nil (s : Nat) {n : Nat} : range' s n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem range'_zero : range' s 0 step = [] := by
+@[simp] theorem range'_zero : range' s 0 = [] := by
   simp
 
 @[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
 
-@[simp] theorem tail_range' (n : Nat) : (range' s n step).tail = range' (s + step) (n - 1) step := by
-  cases n with
-  | zero => simp
-  | succ n => simp [range'_succ]
-
 @[simp] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
   constructor
   · intro h
@@ -158,9 +153,6 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
 theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem tail_range (n : Nat) : (range n).tail = range' 1 (n - 1) := by
-  rw [range_eq_range', tail_range']
-
 @[simp]
 theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_sublist_right]
@@ -227,12 +219,6 @@ theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).len
   simp only [getElem?_enumFrom, getElem?_eq_getElem h]
   simp
 
-@[simp]
-theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by
-  induction l generalizing n with
-  | nil => simp
-  | cons _ l ih => simp [ih, enumFrom_cons]
-
 theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
     map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
   ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl

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_left hn).symm
+  exact (List.getElem_append n hn).symm
 
 -- See `Init.Data.List.Nat.Sublist` for `IsSuffix.getElem`.
 

src/Init/Data/List/Zip.lean

@@ -31,10 +31,6 @@ theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
 theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
     zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
 
-@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
-    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
-  cases l₁ <;> cases l₂ <;> simp
-
 theorem zip_append :
     ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
       zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
@@ -233,7 +229,6 @@ theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n
 
 @[deprecated drop_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_drop := @drop_zipWith
 
-@[simp]
 theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
   rw [← drop_one]; simp [drop_zipWith]
 
@@ -289,16 +284,12 @@ theorem head?_zipWithAll {f : Option α → Option β → γ} :
       | none, none => .none | a?, b? => some (f a? b?) := by
   simp [head?_eq_getElem?, getElem?_zipWithAll]
 
-@[simp] theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
+theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
     (zipWithAll f as bs).head h = f as.head? bs.head? := by
   apply Option.some.inj
   rw [← head?_eq_head, head?_zipWithAll]
   split <;> simp_all
 
-@[simp] theorem tail_zipWithAll {f : Option α → Option β → γ} :
-    (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail := by
-  cases as <;> cases bs <;> simp
-
 theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
     zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
@@ -367,12 +358,6 @@ theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp
     (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
   rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by
-  cases l <;> simp
-
-@[simp] theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by
-  cases l <;> simp
-
 @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp

src/Init/Data/Nat/Basic.lean

@@ -722,7 +722,7 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
 
 theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
-instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩
+instance {n : Nat} : NeZero (succ n) := ⟨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 = !(testBit x 0) := by
+private theorem testBit_succ_zero : testBit (x + 1) 0 = not (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 = !(testBit x i) := by
+theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = not (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/Option/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Mario Carneiro
 prelude
 import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
-import Init.Data.BEq
 import Init.Classical
 import Init.Ext
 
@@ -248,7 +247,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
 
-theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
+@[simp] 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 α} :
@@ -412,37 +411,6 @@ 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,17 +290,11 @@ 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⟩
+def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' n usize_size_gt_zero⟩
 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 Bool.or (x y : Bool) : Bool :=
+@[macro_inline] def 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 Bool.and (x y : Bool) : Bool :=
+@[macro_inline] def and (x y : Bool) : Bool :=
   match x with
   | false => false
   | true  => y
@@ -1034,12 +1034,10 @@ 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 Bool.not : Bool → Bool
+@[inline] def 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 => ! ps[i]!.borrow
+  isBorrowParamAux x ys fun i => not 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 => ! ps[i]!.borrow) b liveVarsAfter
+  addIncBeforeAux ctx xs (fun i => not 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 (!b))
-  pure (!b)
+  let b ← anyM a (fun v => do let b ← p v; pure (not b))
+  pure (not 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 !(has_lt && all_le) then continue
+      if not (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⟩
-  | Bool.not subExpr =>
+  | 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⟩
-  | 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
+  | 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
   | 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 (!skipAuxDecl)
+        guard (not 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 && !projs.isEmpty) with
+    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && not 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 !(← isDefEq a.getAppFn b.getAppFn) then
+      else if not (← 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 !(← isType a)
+      return not (← 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 !(← hasLetDeclsInBetween) then
+  if not (← 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 !(← isType a)
+      return not (← isType a)
     else
       isProof a
   else

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -199,8 +199,9 @@ Performs a possibly type-changing transformation to a `MatcherApp`.
 If `useSplitter` is true, the matcher is replaced with the splitter.
 NB: Not all operations on `MatcherApp` can handle one `matcherName` is a splitter.
 
-If `addEqualities` is true, then equalities connecting the discriminant to the parameters of the
-alternative (like in `match h : x with …`) are be added, if not already there.
+The array `addEqualities`, if provided, indicates for which of the discriminants an equality
+connecting the discriminant to the parameters of the alternative (like in `match h : x with …`)
+should be added (if it is isn't already there).
 
 This function works even if the the type of alternatives do *not* fit the inferred type. This
 allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will
@@ -211,13 +212,20 @@ def transform
     [AddMessageContext n] [MonadOptions n]
     (matcherApp : MatcherApp)
     (useSplitter := false)
-    (addEqualities : Bool := false)
+    (addEqualities : Array Bool := mkArray matcherApp.discrs.size false)
     (onParams : Expr → n Expr := pure)
     (onMotive : Array Expr → Expr → n Expr := fun _ e => pure e)
     (onAlt : Expr → Expr → n Expr := fun _ e => pure e)
     (onRemaining : Array Expr → n (Array Expr) := pure) :
     n MatcherApp := do
 
+  if addEqualities.size != matcherApp.discrs.size then
+    throwError "MatcherApp.transform: addEqualities has wrong size"
+
+  -- Do not add equalities when the matcher already does so
+  let addEqualities := Array.zipWith addEqualities matcherApp.discrInfos fun b di =>
+    if di.hName?.isSome then false else b
+
   -- We also handle CasesOn applications here, and need to treat them specially in a
   -- few places.
   -- TODO: Expand MatcherApp with the necessary fields to make this more uniform
@@ -233,26 +241,17 @@ def transform
   let params' ← matcherApp.params.mapM onParams
   let discrs' ← matcherApp.discrs.mapM onParams
 
-  let (motive', uElim, addHEqualities) ← lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
+
+  let (motive', uElim) ← lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
     unless motiveArgs.size == matcherApp.discrs.size do
       throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
     let mut motiveBody' ← onMotive motiveArgs motiveBody
 
-    -- Prepend `(x = e) →` or `(HEq x e) → ` to the motive when an equality is requested
-    -- and not already present, and remember whether we added an Eq or a HEq
-    let mut addHEqualities : Array (Option Bool) := #[]
-    for arg in motiveArgs, discr in discrs', di in matcherApp.discrInfos do
-      if addEqualities && di.hName?.isNone then
-        if ← isProof arg then
-          addHEqualities := addHEqualities.push none
-        else
-          let heq ← mkEqHEq discr arg
-          motiveBody' ← liftMetaM <| mkArrow heq motiveBody'
-          addHEqualities := addHEqualities.push heq.isHEq
-      else
-        addHEqualities := addHEqualities.push none
+    -- Prepend (x = e) → to the motive when an equality is requested
+    for arg in motiveArgs, discr in discrs', b in addEqualities do if b then
+      motiveBody' ← liftMetaM <| mkArrow (← mkEq discr arg) motiveBody'
 
-    return (← mkLambdaFVars motiveArgs motiveBody', ← getLevel motiveBody', addHEqualities)
+    return (← mkLambdaFVars motiveArgs motiveBody', ← getLevel motiveBody')
 
   let matcherLevels ← match matcherApp.uElimPos? with
     | none     => pure matcherApp.matcherLevels
@@ -262,14 +261,15 @@ def transform
   -- (and count them along the way)
   let mut remaining' := #[]
   let mut extraEqualities : Nat := 0
-  for discr in discrs'.reverse, b in addHEqualities.reverse do
-    match b with
-    | none => pure ()
-    | some is_heq =>
-        remaining' := remaining'.push (← (if is_heq then mkHEqRefl else mkEqRefl) discr)
-        extraEqualities := extraEqualities + 1
+  for discr in discrs'.reverse, b in addEqualities.reverse do if b then
+    remaining' := remaining'.push (← mkEqRefl discr)
+    extraEqualities := extraEqualities + 1
 
   if useSplitter && !isCasesOn then
+    -- We replace the matcher with the splitter
+    let matchEqns ← Match.getEquationsFor matcherApp.matcherName
+    let splitter := matchEqns.splitterName
+
     let aux1 := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params'
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
@@ -278,10 +278,6 @@ def transform
       check aux1
     let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1
 
-    -- We replace the matcher with the splitter
-    let matchEqns ← Match.getEquationsFor matcherApp.matcherName
-    let splitter := matchEqns.splitterName
-
     let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params'
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'

src/Lean/Meta/Tactic/FunInd.lean

@@ -8,6 +8,7 @@ prelude
 import Lean.Meta.Basic
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Check
+import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
@@ -401,51 +402,19 @@ def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
     mvarid ← mvarid.assert (.mkSimple s!"ih{i+1}") (← inferType v) v
   return mvarid
 
+
 /--
-Goal cleanup:
-Substitutes equations (with `substVar`) to remove superfluous varialbes, and clears unused
-let bindings.
-
-Substitutes from the outside in so that the inner-bound variable name wins, but does a first pass
-looking only at variables with names with macro scope, so that preferably they disappear.
-
-Careful to only touch the context after the motives (given by the index) as the motive could depend
-on anything before, and `substVar` would happily drop equations about these fixed parameters.
+Substitutes equations, but makes sure to only substitute variables introduced after the motives
+(given by the index) as the motive could depend on anything before, and `substVar` would happily
+drop equations about these fixed parameters.
 -/
-partial def cleanupAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
-  let mvarId ← go mvarId index true
-  let mvarId ← go mvarId index false
-  return mvarId
-where
-  go (mvarId : MVarId) (index : Nat) (firstPass : Bool) : MetaM MVarId := do
-    if let some mvarId ← cleanupAfter? mvarId index firstPass then
-      go mvarId index firstPass
-    else
-      return mvarId
-
-  allHeqToEq (mvarId : MVarId) (index : Nat) : MetaM MVarId :=
-    mvarId.withContext do
-      let mut mvarId := mvarId
-      for localDecl in (← getLCtx) do
-        if localDecl.index > index then
-          let (_, mvarId') ← heqToEq mvarId localDecl.fvarId
-          mvarId := mvarId'
-      return mvarId
-
-  cleanupAfter? (mvarId : MVarId) (index : Nat) (firstPass : Bool)  : MetaM (Option MVarId) := do
-    mvarId.withContext do
-      for localDecl in (← getLCtx) do
-        if localDecl.index > index && (!firstPass || localDecl.userName.hasMacroScopes) then
-          if localDecl.isLet then
-            if let some mvarId' ← observing? <| mvarId.clear localDecl.fvarId then
-              return some mvarId'
-          if let some mvarId' ← substVar? mvarId localDecl.fvarId then
-            -- After substituting, some HEq might turn into Eqs, and we want to be able to substitute
-            -- them as well
-            let mvarId' ← allHeqToEq mvarId' index
-            return some mvarId'
-      return none
-
+def substVarAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
+  mvarId.withContext do
+    let mut mvarId := mvarId
+    for localDecl in (← getLCtx) do
+      if localDecl.index > index then
+        mvarId ← trySubstVar mvarId localDecl.fvarId
+    return mvarId
 
 /--
 Second helper monad collecting the cases as mvars
@@ -460,7 +429,7 @@ def M2.branch {α} (act : M2 α) : M2 α :=
 
 
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis.  -/
-def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toClear : Array FVarId)
+def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toClear toPreserve : Array FVarId)
     (goal : Expr)  (e : Expr) : M2 Expr := do
   let _e' ← foldAndCollect oldIH newIH isRecCall e
   let IHs : Array Expr ← M.ask
@@ -472,6 +441,8 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
   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
@@ -486,7 +457,7 @@ Like `mkLambdaFVars (usedOnly := true)`, but
 The result `r` can be applied with `r.beta (maskArray mask args)`.
 
 We use this when generating the functional induction principle to refine the goal through a `match`,
-here `xs` are the discriminants of the `match`.
+here `xs` are the discriminans of the `match`.
 We do not expect non-trivial discriminants to appear in the goal (and if they do, the user will
 get a helpful equality into the context).
 -/
@@ -516,7 +487,7 @@ Builds an expression of type `goal` by replicating the expression `e` into its t
 where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
 as `MVars` as it goes.
 -/
-partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
+partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
     (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M2 Expr := do
 
   -- if-then-else cause case split:
@@ -525,10 +496,10 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     let c' ← foldAndCollect oldIH newIH isRecCall c
     let h' ← foldAndCollect oldIH newIH isRecCall h
     let t' ← withLocalDecl `h .default c' fun h => M2.branch do
-      let t' ← buildInductionBody toClear goal oldIH newIH isRecCall t
+      let t' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
-      let f' ← buildInductionBody toClear goal oldIH newIH isRecCall f
+      let f' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -537,11 +508,11 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     let h' ← foldAndCollect oldIH newIH isRecCall h
     let t' ← withLocalDecl `h .default c' fun h => M2.branch do
       let t ← instantiateLambda t #[h]
-      let t' ← buildInductionBody toClear goal oldIH newIH isRecCall t
+      let t' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
       let f ← instantiateLambda f #[h]
-      let f' ← buildInductionBody toClear goal oldIH newIH isRecCall f
+      let f' ← buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -552,8 +523,8 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
   match_expr goal with
   | And goal₁ goal₂ => match_expr e with
     | PProd.mk _α _β e₁ e₂ =>
-      let e₁' ← buildInductionBody toClear goal₁ oldIH newIH isRecCall e₁
-      let e₂' ← buildInductionBody toClear goal₂ oldIH newIH isRecCall e₂
+      let e₁' ← buildInductionBody toClear toPreserve goal₁ oldIH newIH isRecCall e₁
+      let e₂' ← buildInductionBody toClear toPreserve goal₂ oldIH newIH isRecCall e₂
       return mkApp4 (.const ``And.intro []) goal₁ goal₂ e₁' e₂'
     | _ =>
       throwError "Goal is PProd, but expression is:{indentExpr e}"
@@ -572,14 +543,14 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     -- so we need to replace that IH
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform (useSplitter := true)
-        (addEqualities := true)
+        (addEqualities := mask.map not)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => M2.branch do
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let alt' ← buildInductionBody (toClear.push newIH'.fvarId!) goal' oldIH' newIH'.fvarId! isRecCall alt
+              let alt' ← buildInductionBody (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! isRecCall alt
               mkLambdaFVars #[newIH'] alt')
         (onRemaining := fun _ => pure #[.fvar newIH])
       return matcherApp'.toExpr
@@ -591,34 +562,32 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
       let (mask, absMotiveBody) ← mkLambdaFVarsMasked matcherApp.discrs goal
 
       let matcherApp' ← matcherApp.transform (useSplitter := true)
-        (addEqualities := true)
+        (addEqualities := mask.map not)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => M2.branch do
-          buildInductionBody toClear expAltType oldIH newIH isRecCall alt)
+          buildInductionBody toClear toPreserve expAltType oldIH newIH isRecCall alt)
       return matcherApp'.toExpr
 
   if let .letE n t v b _ := e then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
     return ← withLetDecl n t' v' fun x => M2.branch do
-      let b' ← buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
+      let b' ← buildInductionBody toClear toPreserve goal oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFVars #[x] b'
 
   if let some (n, t, v, b) := e.letFun? then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
     return ← withLocalDecl n .default t' fun x => M2.branch do
-      let b' ← buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
+      let b' ← buildInductionBody toClear toPreserve goal oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFun x v' b'
 
-  liftM <| buildInductionCase oldIH newIH isRecCall toClear goal e
+  liftM <| buildInductionCase oldIH newIH isRecCall toClear toPreserve goal e
 
 /--
-Given an expression `e` with metavariables `mvars`
-* performs more cleanup:
-  * removes unused let-expressions after index `index`
-  * tries to substitute variables after index `index`
+Given an expression `e` with metavariables
+* collects all these meta-variables,
 * lifts them to the current context by reverting all local declarations after index `index`
 * introducing a local variable for each of the meta variable
 * assigning that local variable to the mvar
@@ -636,7 +605,7 @@ do not handle delayed assignemnts correctly.
 def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do
   trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}"
   let mvars ← mvars.mapM fun mvar => do
-    let mvar ← cleanupAfter mvar index
+    let mvar ← substVarAfter mvar index
     mvar.withContext do
       let fvarIds := (← getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl => fvarIds.push decl.fvarId
       let (_, mvar) ← mvar.revert fvarIds
@@ -693,7 +662,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
             let body ← instantiateLambda body targets
             removeLamda body fun oldIH body => do
               let body ← instantiateLambda body extraParams
-              let body' ← buildInductionBody #[genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
+              let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
               if body'.containsFVar oldIH then
                 throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
               mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
@@ -1003,7 +972,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
                 removeLamda body fun oldIH body => do
                   trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}"
                   let body ← instantiateLambda body extraParams
-                  let body' ← buildInductionBody #[genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
+                  let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
                   if body'.containsFVar oldIH then
                     throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
                   mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')

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

@@ -77,9 +77,8 @@ 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
-    have : NeZero n := ⟨h⟩
-    return .done <| toExpr (Fin.ofNat' n v)
+  if h : n > 0 then
+    return .done <| toExpr (Fin.ofNat' v h)
   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 !(← returnsPi motive) && !(← isNonConstFun motive)
+  return not (← returnsPi motive) && not (← 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 !(i < args.size) then return ()
+    if not (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 !(← read).knowsType then
+  if not (← 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 !rest.isEmpty then
+      if not 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 !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
-        if !(← isHigherOrder (← inferType args[i]!)) then continue
+        if not (bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
+        if not (← isHigherOrder (← inferType args[i]!)) then continue
         if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue
 
-        if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && !(← valUnknown mvars[i]!)
+        if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && not (← 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 (!(← typeUnknown mvars[i]!)) true analyze
+          if (← get).provideds[i]! then withKnowing (not (← typeUnknown mvars[i]!)) true analyze
           tryUnify mvars[i]! args[i]!
 
     maybeSetExplicit := do

src/Std/Data/DHashMap/Basic.lean

@@ -186,15 +186,6 @@ section Unverified
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : (a : α) → β a → Bool)
-    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
-  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
-    if f a b then
-      (l.insert a b, r)
-    else
-      (l, r.insert a b)
-
 @[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f

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_left' (l₂ := self[i] :: l₂), getElem_congr_coll h₁.symm]
+      rw [← List.getElem_append (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/HashMap/Basic.lean

@@ -190,11 +190,6 @@ section Unverified
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
-@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
-    (m : HashMap α β) : HashMap α β × HashMap α β :=
-  let ⟨l, r⟩ := m.inner.partition f
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 @[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init

src/Std/Data/HashSet/Basic.lean

@@ -158,11 +158,6 @@ section Unverified
 @[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
-  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.

src/Std/Sat/CNF/Literal.lean

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

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

@@ -37,11 +37,15 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
 theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderCarry aig input, assign⟧
       =
-      ((xor
+    or
+      (and
+        (xor
           ⟦aig, input.lhs, assign⟧
-          ⟦aig, input.rhs, assign⟧) &&
-        ⟦aig, input.cin, assign⟧ ||
-       ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)
+          ⟦aig, input.rhs, assign⟧)
+        ⟦aig, input.cin, assign⟧)
+      (and
+        ⟦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 => Bool.xor
+  | xor => _root_.xor
   | beq => (· == ·)
   | imp => (!· || ·)
 

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

@@ -21,11 +21,12 @@ 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] at pl
-    simp at pl
+    rw [sat_iff, h, not.eq_def] at pl
+    split at pl <;> simp_all
   · intro h
     rw [sat_iff] at h
-    cases h : p l.fst <;> simp_all
+    rw [not.eq_def]
+    split <;> 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, !l.2) then
+  if heq1 : c.clause.contains (l.1, not 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 !l.2 then
+        if not 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 !l.2 then
+        if not 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 !derivedEmpty then
+    else if not 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 || !derivedEmpty then (f, false)
+          if encounteredError || not 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 !allChecksPassed then (f, false)
+        if not 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] at l_ne_b
-              simp at l_ne_b
+              simp only [← heq, not] at l_ne_b
+              split 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, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
-        simp_all
+        simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
+        split 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, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
-        simp_all
+        simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
+        split 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) :
-    (Bool.xor lhs' rhs') = (xor lhs rhs) := by
+    (xor lhs' rhs') = (xor lhs rhs) := by
   simp[*]
 
 theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :