perf: add `ShareCommon.shareCommon'` (#4767)

A more restrictive but efficient max sharing primitive.

**Motivation:** Some software verification proofs may contain
significant redundancy that can be eliminated using hash-consing (also
known as `shareCommon`). For example, [theorem
`sha512_block_armv8_test_4_sym`](https://github.com/leanprover/LNSym/blob/460fe5d74cb1907ab64bafce51903d6d1daf0bce/Proofs/SHA512/SHA512Sym.lean#L29)
took a few seconds at [`addPreDefinitions`
](https://github.com/leanprover/lean4/blob/1a12f63f742a578a514536ef45cf9df0c9793af0/src/Lean/Elab/PreDefinition/Main.lean#L155)
and one second at `fixLevelParams` on a MacBook Pro (with M1 Pro). The
proof term initially had over 16 million subterms, but the redundancy
was indirectly and inefficiently eliminated using `Core.transform` at
`addPreDefinitions`. I tried to use `shareCommon` method to fix the
performance issue, but it was too inefficient. This PR introduces a new
`shareCommon'` method that, although less flexible (e.g., it uses only a
local cache and hash-consing table), is much more efficient. The new
procedure minimizes the number of RC operations and optimizes the
caching strategy. It is 20 times faster than the old `shareCommon`
procedure for theorem `sha512_block_armv8_test_4_sym`.