chore(hammer branch): bump v4.21.0

[hanwenzhu]

This PR introduces the following changes:

• Name deprecation of Fin.ofNat' -> Fin.ofNat
• Lean core changed the signature of Lean.Meta.AbstractMVarsResult, renaming its numMVars field to mvars. This created a conflict in the function e.g. Auto.abstractMVars. In fixing this issue, I found that Auto.abstractMVars probably intended to use the custom Auto.AbstractMVars.AbstractMVarsResult instead of Lean.Meta.AbstractMVarsResult anyway, so I changed the signatures to use the former. The long-term solution would be to use only Lean.Meta.AbstractMVarsResult, but per my understanding the current one is used for a bug fix?
• Lean core added an abstraction MonadDeclNameGenerator for generating auxiliary declaration names. As a result, the Lean.mkAuxDecl function is removed. I tried to modify Lean-auto to use the intended consequence of this abstraction in Lean core, which is to remove the field declName? in Reif.ReifM and rely on the (automatic) instance MonadDeclNameGenerator Reif.ReifM instead. (For example see the corresponding change in GrindM in the linked commit above).
• I cherry-picked the removal of MathlibEmulator/Basic from lean-auto:main. This change was written by Yicheng and is due to an error report that Lean-auto does not build with Mathlib by Kim (see Zulip).
• Lean bump to v4.21.0.