mathlib

92b29c77 - fix(tactic/norm_num): make norm_num user command match norm_num better (#12667)

fix(tactic/norm_num): make norm_num user command match norm_num better (#12667) Corrects some issues with the `#norm_num` user command that prevented it from fully normalizing expressions. Also, adds `expr.norm_num`.