From 3e0ea7fbae4d6b3075b35815303a890eb4875657 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Feb 2022 16:25:33 -0800
Subject: [PATCH] fix: use `instantiateMVars` before invoking pure function
 `findIfToSplit`

---
 src/Lean/Meta/Tactic/SplitIf.lean | 1 +
 1 file changed, 1 insertion(+)

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