diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index ed92ba713f..c6c4b1ec0a 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -137,7 +137,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
                   mkLambdaFVars (ys++altEqsNew) body
             altsNew := altsNew.push altNew
           return .done { matcherApp with alts := altsNew }.toExpr
-        transform e pre
+        transform (← instantiateMVars e) pre
       let targetNew ← mkNewTarget (← getMVarType mvarId)
       unless (← foundRef.get) do
         throwError "'applyMatchSplitter' failed, did not find discriminants"
diff --git a/tests/lean/run/1168.lean b/tests/lean/run/1168.lean
new file mode 100644
index 0000000000..0a0be0e0ce
--- /dev/null
+++ b/tests/lean/run/1168.lean
@@ -0,0 +1,3 @@
+theorem ex : True ∧ (match True with | _ => True) := by
+  constructor; exact trivial
+  split; trivial