Bump std

[tobiasgrosser]

The main differences to fix are:

• simp became less aggressive and we have to use zetaDelta := true to obtain the original behavior
• generalize unfolds less and we introduce our own generalize! to keep the old behavior
• BitVec moved to lean4 itself and the definition of BitVec.ofInt changed
• Mathlib's library search changed, so we drop it for now
• The syntax became less permissive in case of broken indentation. We consequently fix our indentation.

[tobiasgrosser]

This PR has still two unfinished sorries.

[tobiasgrosser]

The following tasks are still open:

one BitVec proof does not go through, due to casts

   -- rw [xxx] -- This should go through, but does not due to casting issues.
        have yy : 2 ^ w - 1 < (2 ^ w + 1) / 2 := by sorry

Some of the BitVec proofs are rather verbose.

[tobiasgrosser]

I merged this as the deadline now has passed.