Removing `Nat.bitwise'` in favor of `Nat.bitwise`

Stream: mathlib4

[Alex Keizer]

There has been a bit of discussion surrounding Nat.bitwise and Nat.bitwise'. The docstring of the later (in Mathlib) has the following to say

-- Porting note: There is a `Nat.bitwise` in Lean 4 core,
-- but it is different from the one in mathlib3, so we just port blindly here.
/-- `Nat.bitwise'` (different from `Nat.bitwise` in Lean 4 core)
  applies the function `f` to pairs of bits in the same position in
  the binary representations of its inputs. -/

However, as part of #5920, we now have a proof that bitwise and bitwise' are actually equal. Would it make sense to just remove the mathlib version (bitwise') and move every use of it to core's bitwise?
I think @Eric Wieser already expressed a preference to go this direction.

[Eric Wieser]

(docs#Nat.bitwise, docs#Nat.bitwise')

[Eric Wieser]

Whatever happens, I think in the short term it would be great to merge your proof (in a new standalone PR) that the two are equal.

[Ruben Van de Velde]

Earlier discussion

[Ruben Van de Velde]

And https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/data.2Enat.2Ebits

[Eric Wieser]

I think that first link is broken

[Ruben Van de Velde]

(Fixed, I think)

[Alex Keizer]

Going by the linked discussion, @Scott Morrison was the one to propose bitwise' as distinct from bitwise. The main motivation seemed to be that migrating to core's bitwise was proven problematic and that it wasn't worth holding up the port for.
So, it seems there is no problem with merging the two now?

[Alex Keizer]

Eric Wieser said:

Whatever happens, I think in the short term it would be great to merge your proof (in a new standalone PR) that the two are equal.

I extracted that proof in #7410!

[Eric Wieser]

Thanks, I left an initial round of comments

[Alex Keizer]

Thanks for the quick review, I'll have a look tomorrow!

[Eric Wieser]

Worth also noting that this duplication is endemic; we have both docs#Nat.lxor' and docs#Nat.xor, which are equal but the first doesn't have the optimized implementation

[Eric Wieser]

Once the bitwise_eq_bitwise' lemma is in, we can remove all those duplicate definitions, and fix any broken proofs by rewriting by your lemma