chore: bump Std (leanprover-community#10177)

There's an exciting linter failure on `bump/v4.6.0`, and I'm wondering if this is caused by strange simp lemmas in leanprover-community/batteries#558, so I'm updating to that before the bump.



Co-authored-by: Scott Morrison <[email protected]>

Author: kim-em

Mathlib/Data/BitVec/Lemmas.lean

@@ -70,8 +70,6 @@ theorem addLsb_eq_twice_add_one {x b} : addLsb x b = 2 * x + cond b 1 0 := by
 -- Since the statement is awkward and `Std.BitVec` has no comparable API, we just drop it.
 #noalign bitvec.to_nat_eq_foldr_reverse
 
-theorem toNat_lt {n : ℕ} (v : BitVec n) : v.toNat < 2 ^ n := by
-  exact v.toFin.2
 #align bitvec.to_nat_lt Std.BitVec.toNat_lt
 
 theorem addLsb_div_two {x b} : addLsb x b / 2 = x := by
@@ -132,8 +130,6 @@ variable (x y : Fin (2^w))
   simp only [HXor.hXor, Xor.xor, Fin.xor, BitVec.xor, toNat_ofFin, ofFin.injEq, Fin.mk.injEq]
   exact mod_eq_of_lt (Nat.xor_lt_two_pow x.prop y.prop)
 
-@[simp] lemma ofFin_add : ofFin (x + y)   = ofFin x + ofFin y   := rfl
-@[simp] lemma ofFin_sub : ofFin (x - y)   = ofFin x - ofFin y   := rfl
 @[simp] lemma ofFin_mul : ofFin (x * y)   = ofFin x * ofFin y   := rfl
 
 -- These should be simp, but Std's simp-lemmas do not allow this yet.

Mathlib/Data/Fin/Basic.lean

@@ -209,8 +209,6 @@ section Order
 #align fin.is_le Fin.is_le
 #align fin.is_le' Fin.is_le'
 
-theorem lt_iff_val_lt_val {a b : Fin n} : a < b ↔ (a : ℕ) < b :=
-  Iff.rfl
 #align fin.lt_iff_coe_lt_coe Fin.lt_iff_val_lt_val
 
 theorem le_iff_val_le_val {a b : Fin n} : a ≤ b ↔ (a : ℕ) ≤ b :=

Mathlib/Data/Nat/Bitwise.lean

@@ -129,12 +129,10 @@ theorem xor_bit : ∀ a m b n, bit a m ^^^ bit b n = bit (bne a b) (m ^^^ n) :=
 attribute [simp] Nat.testBit_bitwise
 #align nat.test_bit_bitwise Nat.testBit_bitwise
 
-@[simp]
 theorem testBit_lor : ∀ m n k, testBit (m ||| n) k = (testBit m k || testBit n k) :=
   testBit_bitwise rfl
 #align nat.test_bit_lor Nat.testBit_lor
 
-@[simp]
 theorem testBit_land : ∀ m n k, testBit (m &&& n) k = (testBit m k && testBit n k) :=
   testBit_bitwise rfl
 #align nat.test_bit_land Nat.testBit_land

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "bdec3daab8481a5750e255c9bdf8bf087370908b",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",