mathlib

ec322deb - fix(tactic/{norm_num, abel}): do not do syntactic matches on typeclass instances (#18129)

fix(tactic/{norm_num, abel}): do not do syntactic matches on typeclass instances (#18129) Specifically, this remove syntactic matches on `has_pow` and `has_smul` instances in favor of unification. In all cases there is a cache we can exploit to avoid looking up the preferred instance from scratch every time.