feat(data/nat/digits): add norm_digits tactic (#4452)
This adds a basic tactic for normalizing expressions of the form `nat.digits a b = l`. As requested on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/simplifying.20nat.2Edigits/near/212152395
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
