fix: split candidate selection

leanprover · Jul 2, 2024 · d51e86b · d51e86b
1 parent 1479d41
commit d51e86b
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -89,7 +89,7 @@ partial def findSplit? (e : Expr) (kind : SplitKind := .both) (exceptionSet : Ex
 where
   go (e : Expr) : MetaM (Option Expr) := do
     if let some target ← find? e then
-      if e.isIte || e.isDIte then
+      if target.isIte || target.isDIte then
         let cond := target.getArg! 1 5
         -- Try to find a nested `if` in `cond`
         return (← go cond).getD target

diff --git a/tests/lean/run/splitOrderIssue.lean b/tests/lean/run/splitOrderIssue.lean
@@ -0,0 +1,10 @@
+example (b : Bool) : (if (if b then true else true) then 1 else 2) = 1 := by
+  split
+  next h =>
+    guard_target =ₛ (if true = true then 1 else 2) = 1
+    guard_hyp h : b = true
+    simp
+  next h =>
+    guard_target =ₛ (if true = true then 1 else 2) = 1
+    guard_hyp h : ¬b = true
+    simp