From c19672e99ef8d8584f4f6622735cdb21e59a60d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Apr 2022 15:29:39 -0700
Subject: [PATCH] fix: basic support for the new discriminant equality encoding
 at `split`

TODO: This is a temporary fix. We can do better.
---
 src/Lean/Meta/Tactic/Split.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index dc4c51e8c0..f3954b8aa9 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -148,7 +148,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
       let numParams := matchEqns.splitterAltNumParams[i]
       let (_, mvarId) ← introN mvarId numParams
       trace[Meta.Tactic.split] "before unifyEqs\n{mvarId}"
-      match (← Cases.unifyEqs numEqs mvarId {}) with
+      match (← Cases.unifyEqs (numEqs + info.getNumDiscrEqs) mvarId {}) with
       | none   => return (i+1, mvarIds) -- case was solved
       | some (mvarId, _) =>
         let mvarId ← substDiscrEqs mvarId discrEqs