fix: match equality generation (#6719)

This PR fixes a bug in the equational theorem generator for
`match`-expressions. See new test for an example.

Signed-off-by: Leonardo de Moura <leodemoura@amazon.com>
Co-authored-by: Leonardo de Moura <leodemoura@amazon.com>

src/Init/Data/Nat/Linear.lean

@@ -718,8 +718,7 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
 
 end Linear
 
-def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α := by
-  simp_arith at h₁
-  exact h₂ h₁
+def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α :=
+  h₂ (Nat.add_right_cancel h₁)
 
 end Nat

src/Lean/Meta/Match/MatchEqs.lean

@@ -322,6 +322,11 @@ private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := mvarId.with
           | none => pure ()
   throwError "substSomeVar failed"
 
+private def unfoldElimOffset (mvarId : MVarId) : MetaM MVarId := do
+  if Option.isNone <| (← mvarId.getType).find? fun e => e.isConstOf ``Nat.elimOffset then
+    throwError "goal's target does not contain `Nat.elimOffset`"
+  mvarId.deltaTarget (· == ``Nat.elimOffset)
+
 /--
   Helper method for proving a conditional equational theorem associated with an alternative of
   the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. -/
@@ -343,6 +348,8 @@ where
       <|>
       (do mvarId.contradiction { genDiseq := true }; return #[])
       <|>
+      (do let mvarId ← unfoldElimOffset mvarId; return #[mvarId])
+      <|>
       (casesOnStuckLHS mvarId)
       <|>
       (do let mvarId' ← simpIfTarget mvarId (useDecide := true)

tests/lean/run/match_eqns_bug.lean

@@ -0,0 +1,13 @@
+inductive Vec (α : Type u) : Nat → Type u
+  | zero : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
+
+def g (n : Nat) (v w : Vec α n) : Nat :=
+  match v, w with
+  | .zero, _  => 1
+  | _, .cons _ (.cons _ _ ) => 2
+  | _, _ => 3
+
+example (h : g a b c = 4) : False := by
+  unfold g at h
+  split at h <;> contradiction