fix: def+match macro

src/Lean/Elab/MutualDef.lean

@@ -126,7 +126,7 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax :=
 if declVal.isOfKind `Lean.Parser.Command.declValSimple then
   pure $ declVal.getArg 1
 else if declVal.isOfKind `Lean.Parser.Command.declValEqns then
-  expandMatchAltsIntoMatch declVal (declVal.getArg 1)
+  expandMatchAltsIntoMatch declVal (declVal.getArg 0)
 else
   Macro.throwError declVal "unexpected definition value"
 

tests/lean/run/match1.lean

@@ -26,3 +26,11 @@ theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) :=
 by intro
  | Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption }
  | Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ }
+
+inductive C
+| mk₁ : Nat → C
+| mk₂ : Nat → Nat → C
+
+def C.x : C → Nat
+| C.mk₁ x   => x
+| C.mk₂ x _ => x