chore: mark Mul.mul and HMul.hMul as match_pattern

[jcommelin]

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

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e922edfc218090ab2e54092336c67fe3b970dfc2 --onto a35bf7ee4c4d900475d88886825a5337f389bd0f. (2025-01-30 06:19:29)
• ✅ Mathlib branch lean-pr-testing-6863 has successfully built against this PR. (2025-01-30 19:41:12) View Log
• 💥 Mathlib branch lean-pr-testing-6863 build failed against this PR. (2025-01-30 22:27:38) View Log
• 🟡 Mathlib branch lean-pr-testing-6863 build against this PR was cancelled. (2025-01-30 22:59:52) View Log
• 💥 Mathlib branch lean-pr-testing-6863 build failed against this PR. (2025-01-30 23:36:51) View Log
• 🟡 Mathlib branch lean-pr-testing-6863 build against this PR was cancelled. (2025-01-31 05:43:31) View Log
• 🟡 Mathlib branch lean-pr-testing-6863 build against this PR was cancelled. (2025-01-31 05:54:59) View Log
• 🟡 Mathlib branch lean-pr-testing-6863 build this PR didn't complete normally. (2025-01-31 05:55:21) View Log
• 💥 Mathlib branch lean-pr-testing-6863 build failed against this PR. (2025-01-31 06:10:08) View Log

[jcommelin]

An overview of places where this could be used in mathlib:

$ rg -A1 nightly-2024-02-25
Mathlib/Computability/RegularExpressions.lean
95:#adaptation_note /-- nightly-2024-02-25
96-  we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/
--
139:#adaptation_note /-- nightly-2024-02-25
140-  we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/
--
153:#adaptation_note /-- nightly-2024-02-25
154-  we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/
--
346:#adaptation_note /-- nightly-2024-02-25
347-  we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/
--
364:#adaptation_note /-- nightly-2024-02-25
365-  we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/
--
375:#adaptation_note /-- nightly-2024-02-25
376-  we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/
--
386:#adaptation_note /-- nightly-2024-02-25
387-  we need to write `comp x y` in the pattern `comp R S`,

Mathlib/Algebra/Free.lean
83:#adaptation_note /-- nightly-2024-02-25
84-we need to write `mul x y` in the second pattern, instead of `x * y`. --/
--
188:#adaptation_note /-- nightly-2024-02-25
189-we need to write `mul x y` in the second pattern, instead of `x * y`. -/
--
265:#adaptation_note /-- nightly-2024-02-25
266-we need to write `mul x y` in the second pattern, instead of `x * y`. -/
--
282:#adaptation_note /-- nightly-2024-02-25
283-we need to write `mul x y` in the second pattern, instead of `x * y`. -/