diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 81c2241816..095fd09ca5 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -215,7 +215,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
   trace[Meta.Tactic.split] "after introN\n{mvarId}"
   let discrsNew := discrFVarIdsNew.map mkFVar
   let mvarType ← getMVarType mvarId
-  let elimUniv ← getLevel mvarType
+  let elimUniv ← withMVarContext mvarId <| getLevel mvarType
   let us ←
     if let some uElimPos := info.uElimPos? then
       pure <| us.set! uElimPos elimUniv
diff --git a/tests/lean/run/1200.lean b/tests/lean/run/1200.lean
new file mode 100644
index 0000000000..ab113ce2bd
--- /dev/null
+++ b/tests/lean/run/1200.lean
@@ -0,0 +1,6 @@
+example
+(h: match .none (α:=α) with
+| some _ => True
+| _      => True):
+  True := by
+  split at h <;> trivial