matches using `match_pattern` do not generate the right equation lemmas

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When using a match_pattern in a match clause, the equation lemma generated unfolds the match pattern.

Context

#mathlib4 > refactoring WithTop/WithBot as inductive types @ 💬

Steps to Reproduce

1. Run

-- one field structure
structure MyOptionStruct where
  toOption : Option Nat

@[match_pattern]
def MyOptionStruct.some : Nat → MyOptionStruct := fun n => ⟨.some n⟩

@[match_pattern]
def MyOptionStruct.null : MyOptionStruct := ⟨Option.none⟩

def foo : MyOptionStruct → Nat
  | .some n => n
  | .null => 0

theorem wat : foo (.some 1) = 2 := by
  rw [foo] -- fails

#check foo.eq_1

Expected behavior: The rewrite succeeds.

Actual behavior: The rewrite fails, because the equation lemma is about MyOptionStruct.mk.

Versions

[Output of #version or #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the self-contained reproducer in the issue and inspect how equation lemmas are generated for match clauses using match_pattern. Run the wat theorem and check foo.eq_1; done means rw [foo] succeeds without the equation lemma being reduced to MyOptionStruct.mk.