fix: Make split work with metavariables in the target

The fix consists of replacing an internal use of `apply` for
instantiating match splitters by a new, simpler variant `applyN`. This
new `applyN` is not prone to #8436, which is the ultimate cause for
`split` failing on targets containing metavariables.

Author: Sebastian Graf

src/Lean/Meta/Tactic/Apply.lean

@@ -231,6 +231,21 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
 def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvar.apply (← mkConstWithFreshMVarLevels c) cfg (term? := m!"'{.ofConstName c}'")
 
+/-- Close the given goal using `e`, instantiated with `n` metavariables. -/
+def _root_.Lean.MVarId.applyN (mvarId : MVarId) (e : Expr) (n : Nat) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `apply
+    let targetType ← mvarId.getType
+    let eType      ← inferType e
+    let (mvarIds, _, eType) ← forallMetaBoundedTelescope eType n
+    unless mvarIds.size == n do
+      throwError "Applied type takes fewer than {n} arguments:\n{indentExpr eType}"
+    unless (← isDefEqApply cfg eType targetType) do
+      throwError "Type mismatch: target is\n{indentExpr targetType}\nbut applied expression has \
+        type\n{indentExpr eType}\nafter applying {n} arguments."
+    mvarId.assign (e.beta mvarIds)
+    return (mvarIds.map (·.mvarId!)).toList
+
 end Meta
 
 open Meta

src/Lean/Meta/Tactic/Split.lean

@@ -248,9 +248,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
     let splitter := mkAppN (mkApp splitter motive) discrsNew
     check splitter
     trace[split.debug] "after check splitter"
-    let mvarIds ← mvarId.apply splitter
-    unless mvarIds.length == matchEqns.size do
-      throwError "internal error in `split` tactic: unexpected number of goals created after applying splitter auxiliary theorem `{matchEqns.splitterName}` for `{matcherDeclName}`"
+    let mvarIds ← mvarId.applyN splitter matchEqns.size
     let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do
       let numParams := matchEqns.splitterAltNumParams[i]!
       let (_, mvarId) ← mvarId.introN numParams

tests/lean/split_mvars_target.lean

@@ -0,0 +1,15 @@
+/-!
+Tests that `split` works when there are metavariables in the target.
+-/
+theorem split_subgoals {x : Option Nat × Nat} :
+  match x.fst with
+  | some _ => True
+  | none => True
+  := by
+  have h {P : Prop} {x'} : (x' = 4 ∧ P) → P := by simp
+  apply h
+  split
+  rotate_right
+  · exact 4
+  · trivial
+  · trivial