chore: mark Mul.mul and HMul.hMul as match_pattern (#6863)

This PR allows fixing regressions in mathlib introduced in
nightly-2024-02-25 by allowing the use of `x * y` in match patterns.
There are currently 11 instances in mathlib explicitly flagging the lack
of this match pattern.

This issue was previously pointed out in the following Zulip threads:

-
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Algebra.2EFree/near/321482426
-
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/match_pattern.20attribute.20on.20Mul.2Emul/near/321505298
-
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.40.5Bmatch_pattern.5D.20for.20basic.20binary.20operators/near/423734085
-
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Mul.20match_pattern/near/430635623

src/Init/Prelude.lean

@@ -1551,7 +1551,7 @@ instance instAddNat : Add Nat where
 
 /- We mark the following definitions as pattern to make sure they can be used in recursive equations,
    and reduced by the equation Compiler. -/
-attribute [match_pattern] Nat.add Add.add HAdd.hAdd Neg.neg
+attribute [match_pattern] Nat.add Add.add HAdd.hAdd Neg.neg Mul.mul HMul.hMul
 
 set_option bootstrap.genMatcherCode false in
 /--

tests/lean/run/mul_match_pattern.lean

@@ -0,0 +1,14 @@
+namespace mul_match_pattern
+
+inductive Foo
+  | x
+  | bar (y z : Foo)
+
+instance : Mul Foo where
+  mul := Foo.bar
+
+def quux : Foo → Foo
+  | .x => .x
+  | y * _z => y
+
+end mul_match_pattern