diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 8e8aceaaac..9820e988c4 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -66,6 +66,7 @@ partial def findIfToSplit? (e : Expr) : Option Expr :=
     none
 
 def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do
+  let e ← instantiateMVars e
   if let some cond := findIfToSplit? e then
     let hName ← match hName? with
       | none       => mkFreshUserName `h