From f174687608896d2ed4dc14b0eee77c82006a4cf5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 30 Jun 2024 16:15:04 -0700
Subject: [PATCH 01/13] feat: `Simp.Config.implicitDefEqProofs`

---
 src/Lean/Meta/Tactic/Simp/Rewrite.lean |  8 +++++++-
 tests/lean/run/implicitRflProofs.lean  | 25 +++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/implicitRflProofs.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 9a3d3118c408..b68829fa9bc6 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -108,13 +108,19 @@ where
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
       return false
 
+private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
+  if thm.rfl then
+    return (← getConfig).implicitDefEqProofs
+  else
+    return false
+
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
         return none
-      let proof? ← if thm.rfl then
+      let proof? ← if (← useImplicitDefEqProof thm) then
         pure none
       else
         let proof ← instantiateMVars (mkAppN val xs)
diff --git a/tests/lean/run/implicitRflProofs.lean b/tests/lean/run/implicitRflProofs.lean
new file mode 100644
index 000000000000..69fe2dc58ee7
--- /dev/null
+++ b/tests/lean/run/implicitRflProofs.lean
@@ -0,0 +1,25 @@
+def f (x : Nat) := x + 1
+
+theorem f_eq (x : Nat) : f (x + 1) = x + 2 := rfl
+
+theorem ex1 : f (f (x + 1)) = x + 3 := by
+  simp [f_eq]
+
+/--
+info: theorem ex1 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
+fun {x} =>
+  of_eq_true
+    (Eq.trans (congrArg (fun x_1 => x_1 = x + 3) (Eq.trans (congrArg f (f_eq x)) (f_eq (x + 1)))) (eq_self (x + 1 + 2)))
+-/
+#guard_msgs in
+#print ex1
+
+theorem ex2 : f (f (x + 1)) = x + 3 := by
+  simp (config := { implicitDefEqProofs := true }) [f_eq]
+
+/--
+info: theorem ex2 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
+fun {x} => of_eq_true (eq_self (x + 1 + 2))
+-/
+#guard_msgs in
+#print ex2

From b4502a45b0e2c305cc87ca433c5ce33fa501ca54 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 30 Jun 2024 16:28:11 -0700
Subject: [PATCH 02/13] chore: fix tests

---
 tests/compiler/uset.lean     |  1 -
 tests/lean/1113.lean         |  2 +-
 tests/lean/rfl_simp_thm.lean |  2 +-
 tests/lean/run/simp2.lean    | 13 ++++++++++++-
 tests/lean/run/simp5.lean    | 14 +++++++++++++-
 5 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/tests/compiler/uset.lean b/tests/compiler/uset.lean
index 9562cd710501..d83389f50707 100644
--- a/tests/compiler/uset.lean
+++ b/tests/compiler/uset.lean
@@ -7,4 +7,3 @@ structure Point where
 
 def main : IO Unit :=
   IO.println (Point.right ⟨0, 0⟩).x
-
diff --git a/tests/lean/1113.lean b/tests/lean/1113.lean
index f4036fd1e3a3..0c4035e85a44 100644
--- a/tests/lean/1113.lean
+++ b/tests/lean/1113.lean
@@ -4,7 +4,7 @@ def foo: {n: Nat} → Fin n → Nat
 
 theorem t3 {f: Fin (n+1)}:
   foo f = 0 := by
-  simp only [←Nat.succ_eq_add_one n] at f
+  dsimp only [←Nat.succ_eq_add_one n] at f -- use `dsimp` to ensure we don't copy `f`
   trace_state
   simp only [←Nat.succ_eq_add_one n, foo]
 
diff --git a/tests/lean/rfl_simp_thm.lean b/tests/lean/rfl_simp_thm.lean
index 5f84fab634a4..88e3f12ca0e3 100644
--- a/tests/lean/rfl_simp_thm.lean
+++ b/tests/lean/rfl_simp_thm.lean
@@ -3,6 +3,6 @@ def inc (x : Nat) := x + 1
 @[simp] theorem inc_eq : inc x = x + 1 := rfl
 
 theorem ex (a b : Fin (inc n)) (h : a = b) : b = a := by
-  simp only [inc_eq] at a
+  simp (config := { implicitDefEqProofs := true }) only [inc_eq] at a
   trace_state
   exact h.symm
diff --git a/tests/lean/run/simp2.lean b/tests/lean/run/simp2.lean
index 89f82bdda336..1a133c24e887 100644
--- a/tests/lean/run/simp2.lean
+++ b/tests/lean/run/simp2.lean
@@ -4,7 +4,7 @@ def p (x : Prop) := x
  rfl
 
 theorem ex1 (x : Prop) (h : x) : p x := by
-  simp
+  simp (config := { implicitDefEqProofs := true })
   assumption
 
 /--
@@ -14,6 +14,17 @@ fun x h => id h
 #guard_msgs in
 #print ex1
 
+theorem ex1' (x : Prop) (h : x) : p x := by
+  simp
+  assumption
+
+/--
+info: theorem ex1' : ∀ (x : Prop), x → p x :=
+fun x h => Eq.mpr (id (lemma1 x)) h
+-/
+#guard_msgs in
+#print ex1'
+
 theorem ex2 (x : Prop) (q : Prop → Prop) (h₁ : x) (h₂ : q x = x) : q x := by
   simp [h₂]
   assumption
diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean
index c2163c98aadb..6f48dafb89d4 100644
--- a/tests/lean/run/simp5.lean
+++ b/tests/lean/run/simp5.lean
@@ -8,11 +8,23 @@ theorem ex1 (a b c : α) : f (f a b) c = a := by
 
 /--
 info: theorem ex1.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=
-fun {α} a b c => of_eq_true (eq_self a)
+fun {α} a b c =>
+  of_eq_true
+    (Eq.trans (congrArg (fun x => x = a) (Eq.trans (congrArg (fun x => f x c) (f_Eq a b)) (f_Eq a c))) (eq_self a))
 -/
 #guard_msgs in
 #print ex1
 
+theorem ex1' (a b c : α) : f (f a b) c = a := by
+  simp (config := { implicitDefEqProofs := true }) [f_Eq]
+
+/--
+info: theorem ex1'.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=
+fun {α} a b c => of_eq_true (eq_self a)
+-/
+#guard_msgs in
+#print ex1'
+
 theorem ex2 (p : Nat → Bool) (x : Nat) (h : p x = true) : (if p x then 1 else 2) = 1 := by
   simp [h]
 

From fafa561fbd0ecf6af5a2a234533e91bceff49aa3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 1 Jul 2024 04:41:21 -0700
Subject: [PATCH 03/13] chore: missing `trace[split.failure]`

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

diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index b1f6f7c11d7a..047d0fc8a5ec 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -106,6 +106,7 @@ def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Opt
     let mvarId₁ ← simpIfTarget s₁.mvarId
     let mvarId₂ ← simpIfTarget s₂.mvarId
     if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+      trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}"
       return none
     else
       return some ({ s₁ with mvarId := mvarId₁ }, { s₂ with mvarId := mvarId₂ })
@@ -118,6 +119,7 @@ def splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name
       let mvarId₁ ← simpIfLocalDecl s₁.mvarId fvarId
       let mvarId₂ ← simpIfLocalDecl s₂.mvarId fvarId
       if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+        trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}"
         return none
       else
         return some (mvarId₁, mvarId₂)

From f283b6624716e5b031cd5af1df67beacaa64d1d6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 1 Jul 2024 12:05:18 -0700
Subject: [PATCH 04/13] fix: do not look for `split`-tactic candidates in proof
 terms

We also skip candidates in implicit arguments and binders of lambda expressions

See new test.
---
 src/Lean/Meta/Basic.lean          |   2 +-
 src/Lean/Meta/Tactic/Split.lean   |  37 +---------
 src/Lean/Meta/Tactic/SplitIf.lean | 118 +++++++++++++++++++++++++++---
 tests/lean/run/splitIssue2.lean   |  71 ++++++++++++++++++
 4 files changed, 182 insertions(+), 46 deletions(-)
 create mode 100644 tests/lean/run/splitIssue2.lean

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 9767caa08533..581fe806a206 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -229,7 +229,7 @@ structure ParamInfo where
   hasFwdDeps     : Bool       := false
   /-- `backDeps` contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on. -/
   backDeps       : Array Nat  := #[]
-  /-- `isProp` is true if the parameter is always a proposition. -/
+  /-- `isProp` is true if the parameter type is always a proposition. -/
   isProp         : Bool       := false
   /--
     `isDecInst` is true if the parameter's type is of the form `Decidable ...`.
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index be116ed428e1..c9057df01340 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -269,7 +269,7 @@ def mkDiscrGenErrorMsg (e : Expr) : MessageData :=
 def throwDiscrGenError (e : Expr) : MetaM α :=
   throwError (mkDiscrGenErrorMsg e)
 
-def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
+def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do
   let some app ← matchMatcherApp? e | throwError "internal error in `split` tactic: match application expected{indentExpr e}\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program"
   let matchEqns ← Match.getEquationsFor app.matcherName
   let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs
@@ -278,43 +278,14 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
     return (i+1, mvarId::mvarIds)
   return mvarIds.reverse
 
-/-- Return an `if-then-else` or `match-expr` to split. -/
-partial def findSplit? (env : Environment) (e : Expr) (splitIte := true) (exceptionSet : ExprSet := {}) : Option Expr :=
-  go e
-where
-  go (e : Expr) : Option Expr :=
-    if let some target := e.find? isCandidate then
-      if e.isIte || e.isDIte then
-        let cond := target.getArg! 1 5
-        -- Try to find a nested `if` in `cond`
-        go cond |>.getD target
-      else
-        some target
-    else
-      none
-
-  isCandidate (e : Expr) : Bool := Id.run do
-    if exceptionSet.contains e then
-      false
-    else if splitIte && (e.isIte || e.isDIte) then
-      !(e.getArg! 1 5).hasLooseBVars
-    else if let some info := isMatcherAppCore? env e then
-      let args := e.getAppArgs
-      for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
-        if args[i]!.hasLooseBVars then
-          return false
-      return true
-    else
-      false
-
 end Split
 
 open Split
 
-partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do
+partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e := findSplit? (← getEnv) target splitIte badCases then
+    if let some e ← findSplit? target (if splitIte then .both else .match) badCases then
       if e.isIte || e.isDIte then
         return (← splitIfTarget? mvarId).map fun (s₁, s₂) => [s₁.mvarId, s₂.mvarId]
       else
@@ -333,7 +304,7 @@ partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (L
 
 def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId)) := commitWhenSome? do
   mvarId.withContext do
-    if let some e := findSplit? (← getEnv) (← instantiateMVars (← inferType (mkFVar fvarId))) then
+    if let some e ← findSplit? (← instantiateMVars (← inferType (mkFVar fvarId))) then
       if e.isIte || e.isDIte then
         return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂]
       else
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 047d0fc8a5ec..36a5789a5e28 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -8,6 +8,110 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
+
+inductive SplitKind where
+  | ite | match | both
+
+def SplitKind.considerIte : SplitKind → Bool
+  | .ite | .both => true
+  | _ => false
+
+def SplitKind.considerMatch : SplitKind → Bool
+  | .match | .both => true
+  | _ => false
+
+namespace FindSplitImpl
+
+structure Context where
+  exceptionSet : ExprSet := {}
+  kind : SplitKind := .both
+
+unsafe abbrev FindM := ReaderT Context $ StateT (PtrSet Expr) MetaM
+
+private def isCandidate (env : Environment) (ctx : Context) (e : Expr) : Bool := Id.run do
+  if ctx.exceptionSet.contains e then
+    return false
+  if ctx.kind.considerIte && (e.isIte || e.isDIte) then
+    return !(e.getArg! 1 5).hasLooseBVars
+  if ctx.kind.considerMatch then
+    if let some info := isMatcherAppCore? env e then
+      let args := e.getAppArgs
+      for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
+        if args[i]!.hasLooseBVars then
+          return false
+      return true
+  return false
+
+@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+  if (← get).contains e then
+    failure
+  modify fun s => s.insert e
+
+unsafe def visit (e : Expr) : OptionT FindM Expr := do
+  checkVisited e
+  if isCandidate (← getEnv) (← read) e then
+    return e
+  else
+    -- We do not look for split candidates in proofs.
+    unless e.hasLooseBVars do
+      if (← isProof e) then
+        failure
+    match e with
+    | .lam _ _ b _ | .proj _ _ b -- We do not look for split candidates in the binder of lambdas.
+    | .mdata _ b       => visit b
+    | .forallE _ d b _ => visit d <|> visit b -- We want to look for candidates at `A → B`
+    | .letE _ _ v b _  => visit v <|> visit b
+    | .app ..          => visitApp? e
+    | _                => failure
+where
+  visitApp? (e : Expr) : FindM (Option Expr) :=
+    e.withApp fun f args => do
+    let info ← getFunInfo f
+    for u : i in [0:args.size] do
+      let arg := args[i]
+      if h : i < info.paramInfo.size then
+        let info := info.paramInfo[i]
+        unless info.isProp do
+          if info.isExplicit then
+            let some found ← visit arg | pure ()
+            return found
+      else
+        let some found ← visit arg | pure ()
+        return found
+    visit f
+
+end FindSplitImpl
+
+/-- Return an `if-then-else` or `match-expr` to split. -/
+partial def findSplit? (e : Expr) (kind : SplitKind := .both) (exceptionSet : ExprSet := {}) : MetaM (Option Expr) := do
+  go (← instantiateMVars e)
+where
+  go (e : Expr) : MetaM (Option Expr) := do
+    if let some target ← find? e then
+      if e.isIte || e.isDIte then
+        let cond := target.getArg! 1 5
+        -- Try to find a nested `if` in `cond`
+        return (← go cond).getD target
+      else
+        return some target
+    else
+      return none
+
+  find? (e : Expr) : MetaM (Option Expr) := do
+    let some candidate ← unsafe FindSplitImpl.visit e { kind, exceptionSet } |>.run' mkPtrSet
+      | return none
+    trace[split.debug] "candidate:{indentExpr candidate}"
+    return some candidate
+
+/-- Return the condition and decidable instance of an `if` expression to case split. -/
+private partial def findIfToSplit? (e : Expr) : MetaM (Option (Expr × Expr)) := do
+  if let some iteApp ← findSplit? e .ite then
+    let cond := iteApp.getArg! 1 5
+    let dec := iteApp.getArg! 2 5
+    return (cond, dec)
+  else
+    return none
+
 namespace SplitIf
 
 /--
@@ -62,19 +166,9 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
 def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
   return discharge? (← getLCtx).numIndices useDecide
 
-/-- Return the condition and decidable instance of an `if` expression to case split. -/
-private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) :=
-  if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then
-    let cond := iteApp.getArg! 1 5
-    let dec := iteApp.getArg! 2 5
-    -- Try to find a nested `if` in `cond`
-    findIfToSplit? cond |>.getD (cond, dec)
-  else
-    none
-
-def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do
+def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := mvarId.withContext do
   let e ← instantiateMVars e
-  if let some (cond, decInst) := findIfToSplit? e then
+  if let some (cond, decInst) ← findIfToSplit? e then
     let hName ← match hName? with
       | none       => mkFreshUserName `h
       | some hName => pure hName
diff --git a/tests/lean/run/splitIssue2.lean b/tests/lean/run/splitIssue2.lean
new file mode 100644
index 000000000000..f9d3317793cb
--- /dev/null
+++ b/tests/lean/run/splitIssue2.lean
@@ -0,0 +1,71 @@
+namespace Batteries
+
+/-- Union-find node type -/
+structure UFNode where
+  /-- Parent of node -/
+  parent : Nat
+
+namespace UnionFind
+
+/-- Parent of a union-find node, defaults to self when the node is a root -/
+def parentD (arr : Array UFNode) (i : Nat) : Nat :=
+  if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i
+
+/-- Rank of a union-find node, defaults to 0 when the node is a root -/
+def rankD (arr : Array UFNode) (i : Nat) : Nat := 0
+
+theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := sorry
+
+theorem parentD_set {arr : Array UFNode} {x v i} :
+    parentD (arr.set x v) i = if x.1 = i then v.parent else parentD arr i := by
+  rw [parentD]
+  sorry
+
+end UnionFind
+
+open UnionFind
+
+structure UnionFind where
+  arr : Array UFNode
+
+namespace UnionFind
+
+/-- Size of union-find structure. -/
+@[inline] abbrev size (self : UnionFind) := self.arr.size
+
+/-- Parent of union-find node -/
+abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
+
+theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size :=
+  sorry
+
+/-- Rank of union-find node -/
+abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
+
+/-- Maximum rank of nodes in a union-find structure -/
+noncomputable def rankMax (self : UnionFind) := 0
+
+/-- Root of a union-find node. -/
+def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
+  let y := (self.arr.get x).parent
+  if h : y = x then
+    x
+  else
+    have : self.rankMax - self.rank (self.arr.get x).parent < self.rankMax - self.rank x :=
+      sorry
+    self.root ⟨y, sorry⟩
+termination_by self.rankMax - self.rank x
+
+/-- Root of a union-find node. Returns input if index is out of bounds. -/
+def rootD (self : UnionFind) (x : Nat) : Nat :=
+  if h : x < self.size then self.root ⟨x, h⟩ else x
+
+theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
+  simp only [rootD, Array.data_length, parent_lt]
+  split
+  · simp only [parentD, ↓reduceDIte, *]
+    conv => rhs; rw [root]
+    split
+    · rw [root, dif_pos] <;> simp_all
+    · simp
+  · simp only [not_false_eq_true, parentD_of_not_lt, *]

From 2d892dc9ba459ca6a02d94c85b219674427c7d8b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 1 Jul 2024 18:05:36 -0700
Subject: [PATCH 05/13] fix: `split` candidate selection

---
 src/Lean/Meta/Tactic/SplitIf.lean   |  2 +-
 tests/lean/run/splitOrderIssue.lean | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/splitOrderIssue.lean

diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 36a5789a5e28..97489f9560a5 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -88,7 +88,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
new file mode 100644
index 000000000000..457b31a551a1
--- /dev/null
+++ 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

From 1915cb11cc6b39cc567e5c4b833f24d4ab81e3ce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 19 Jul 2024 08:15:13 -0700
Subject: [PATCH 06/13] chore: fix tests

---
 tests/lean/run/implicitRflProofs.lean | 2 +-
 tests/lean/run/simp2.lean             | 2 +-
 tests/lean/run/simp5.lean             | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/lean/run/implicitRflProofs.lean b/tests/lean/run/implicitRflProofs.lean
index 69fe2dc58ee7..fcf5acb04d49 100644
--- a/tests/lean/run/implicitRflProofs.lean
+++ b/tests/lean/run/implicitRflProofs.lean
@@ -3,7 +3,7 @@ def f (x : Nat) := x + 1
 theorem f_eq (x : Nat) : f (x + 1) = x + 2 := rfl
 
 theorem ex1 : f (f (x + 1)) = x + 3 := by
-  simp [f_eq]
+  simp (config := { implicitDefEqProofs := false }) [f_eq]
 
 /--
 info: theorem ex1 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
diff --git a/tests/lean/run/simp2.lean b/tests/lean/run/simp2.lean
index 1a133c24e887..3d25ff858c85 100644
--- a/tests/lean/run/simp2.lean
+++ b/tests/lean/run/simp2.lean
@@ -15,7 +15,7 @@ fun x h => id h
 #print ex1
 
 theorem ex1' (x : Prop) (h : x) : p x := by
-  simp
+  simp (config := { implicitDefEqProofs := false })
   assumption
 
 /--
diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean
index 6f48dafb89d4..8645b488b3bf 100644
--- a/tests/lean/run/simp5.lean
+++ b/tests/lean/run/simp5.lean
@@ -4,7 +4,7 @@ theorem f_Eq {α} (a b : α) : f a b = a :=
   rfl
 
 theorem ex1 (a b c : α) : f (f a b) c = a := by
-  simp [f_Eq]
+  simp (config := { implicitDefEqProofs := false }) [f_Eq]
 
 /--
 info: theorem ex1.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=

From ca0065096f6e5c0da806cc7d16759489d0130c99 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 28 Nov 2024 09:15:33 -0800
Subject: [PATCH 07/13] chore: update doc string

---
 src/Init/MetaTypes.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index 1221a37e4a51..745c68b0f5fe 100644
--- a/src/Init/MetaTypes.lean
+++ b/src/Init/MetaTypes.lean
@@ -224,7 +224,8 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  This option does not have any effect (yet).
+  If `implicitDefEqProofs := true`, `simp` does not create proof terms when the
+  input and output terms are definitionally equal.
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq

From b7563e1840229df19faafe76b4e7fa6fa210cefc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 28 Nov 2024 09:37:00 -0800
Subject: [PATCH 08/13] chore: update tests

---
 tests/lean/rfl_simp_thm.lean          |  2 +-
 tests/lean/run/implicitRflProofs.lean |  4 ++--
 tests/lean/run/simp2.lean             |  4 ++--
 tests/lean/run/simp5.lean             |  4 ++--
 tests/lean/run/splitIssue2.lean       | 12 ++++++------
 5 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/tests/lean/rfl_simp_thm.lean b/tests/lean/rfl_simp_thm.lean
index 88e3f12ca0e3..f414ea130d79 100644
--- a/tests/lean/rfl_simp_thm.lean
+++ b/tests/lean/rfl_simp_thm.lean
@@ -3,6 +3,6 @@ def inc (x : Nat) := x + 1
 @[simp] theorem inc_eq : inc x = x + 1 := rfl
 
 theorem ex (a b : Fin (inc n)) (h : a = b) : b = a := by
-  simp (config := { implicitDefEqProofs := true }) only [inc_eq] at a
+  simp +implicitDefEqProofs only [inc_eq] at a
   trace_state
   exact h.symm
diff --git a/tests/lean/run/implicitRflProofs.lean b/tests/lean/run/implicitRflProofs.lean
index fcf5acb04d49..aecadfbb8c05 100644
--- a/tests/lean/run/implicitRflProofs.lean
+++ b/tests/lean/run/implicitRflProofs.lean
@@ -3,7 +3,7 @@ def f (x : Nat) := x + 1
 theorem f_eq (x : Nat) : f (x + 1) = x + 2 := rfl
 
 theorem ex1 : f (f (x + 1)) = x + 3 := by
-  simp (config := { implicitDefEqProofs := false }) [f_eq]
+  simp -implicitDefEqProofs [f_eq]
 
 /--
 info: theorem ex1 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
@@ -15,7 +15,7 @@ fun {x} =>
 #print ex1
 
 theorem ex2 : f (f (x + 1)) = x + 3 := by
-  simp (config := { implicitDefEqProofs := true }) [f_eq]
+  simp +implicitDefEqProofs [f_eq]
 
 /--
 info: theorem ex2 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
diff --git a/tests/lean/run/simp2.lean b/tests/lean/run/simp2.lean
index 3d25ff858c85..4a91608e095c 100644
--- a/tests/lean/run/simp2.lean
+++ b/tests/lean/run/simp2.lean
@@ -4,7 +4,7 @@ def p (x : Prop) := x
  rfl
 
 theorem ex1 (x : Prop) (h : x) : p x := by
-  simp (config := { implicitDefEqProofs := true })
+  simp +implicitDefEqProofs
   assumption
 
 /--
@@ -15,7 +15,7 @@ fun x h => id h
 #print ex1
 
 theorem ex1' (x : Prop) (h : x) : p x := by
-  simp (config := { implicitDefEqProofs := false })
+  simp -implicitDefEqProofs
   assumption
 
 /--
diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean
index 8645b488b3bf..5d77b52d0096 100644
--- a/tests/lean/run/simp5.lean
+++ b/tests/lean/run/simp5.lean
@@ -4,7 +4,7 @@ theorem f_Eq {α} (a b : α) : f a b = a :=
   rfl
 
 theorem ex1 (a b c : α) : f (f a b) c = a := by
-  simp (config := { implicitDefEqProofs := false }) [f_Eq]
+  simp -implicitDefEqProofs [f_Eq]
 
 /--
 info: theorem ex1.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=
@@ -16,7 +16,7 @@ fun {α} a b c =>
 #print ex1
 
 theorem ex1' (a b c : α) : f (f a b) c = a := by
-  simp (config := { implicitDefEqProofs := true }) [f_Eq]
+  simp +implicitDefEqProofs [f_Eq]
 
 /--
 info: theorem ex1'.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=
diff --git a/tests/lean/run/splitIssue2.lean b/tests/lean/run/splitIssue2.lean
index f9d3317793cb..b35c1c122b7b 100644
--- a/tests/lean/run/splitIssue2.lean
+++ b/tests/lean/run/splitIssue2.lean
@@ -9,15 +9,15 @@ namespace UnionFind
 
 /-- Parent of a union-find node, defaults to self when the node is a root -/
 def parentD (arr : Array UFNode) (i : Nat) : Nat :=
-  if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i
+  if h : i < arr.size then (arr.get i h).parent else i
 
 /-- Rank of a union-find node, defaults to 0 when the node is a root -/
 def rankD (arr : Array UFNode) (i : Nat) : Nat := 0
 
 theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := sorry
 
-theorem parentD_set {arr : Array UFNode} {x v i} :
-    parentD (arr.set x v) i = if x.1 = i then v.parent else parentD arr i := by
+theorem parentD_set {arr : Array UFNode} {x h v i} :
+    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
   rw [parentD]
   sorry
 
@@ -47,11 +47,11 @@ noncomputable def rankMax (self : UnionFind) := 0
 
 /-- Root of a union-find node. -/
 def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
-  let y := (self.arr.get x).parent
+  let y := (self.arr.get x.1 x.2).parent
   if h : y = x then
     x
   else
-    have : self.rankMax - self.rank (self.arr.get x).parent < self.rankMax - self.rank x :=
+    have : self.rankMax - self.rank (self.arr.get x.1 x.2).parent < self.rankMax - self.rank x :=
       sorry
     self.root ⟨y, sorry⟩
 termination_by self.rankMax - self.rank x
@@ -61,7 +61,7 @@ def rootD (self : UnionFind) (x : Nat) : Nat :=
   if h : x < self.size then self.root ⟨x, h⟩ else x
 
 theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
-  simp only [rootD, Array.data_length, parent_lt]
+  simp only [rootD, Array.length_toList, parent_lt]
   split
   · simp only [parentD, ↓reduceDIte, *]
     conv => rhs; rw [root]

From e4d4dc45fb4a9a827165409fe6945eb85c440f50 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 29 Nov 2024 12:44:42 +1100
Subject: [PATCH 09/13] chore: add regression test for earlier slowdown

---
 tests/lean/run/4595_slowdown.lean | 288 ++++++++++++++++++++++++++++++
 1 file changed, 288 insertions(+)
 create mode 100644 tests/lean/run/4595_slowdown.lean

diff --git a/tests/lean/run/4595_slowdown.lean b/tests/lean/run/4595_slowdown.lean
new file mode 100644
index 000000000000..3c1e2d9c5506
--- /dev/null
+++ b/tests/lean/run/4595_slowdown.lean
@@ -0,0 +1,288 @@
+-- The final declaration blew up by a factor of about 40x heartbeats on an earlier draft of
+-- https://github.com/leanprover/lean4/pull/4595, so this is here as a regression test.
+
+universe v v₁ v₂ v₃ u u₁ u₂ u₃
+
+section Mathlib.Combinatorics.Quiver.Basic
+
+class Quiver (V : Type u) where
+  Hom : V → V → Sort v
+
+infixr:10 " ⟶ " => Quiver.Hom
+
+structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
+  obj : V → W
+  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)
+
+end Mathlib.Combinatorics.Quiver.Basic
+
+section Mathlib.CategoryTheory.Category.Basic
+
+namespace CategoryTheory
+
+class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+  id : ∀ X : obj, Hom X X
+  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
+
+scoped notation "𝟙" => CategoryStruct.id
+
+scoped infixr:80 " ≫ " => CategoryStruct.comp
+
+class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+  id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
+  comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Category.Basic
+
+section Mathlib.CategoryTheory.Functor.Basic
+
+namespace CategoryTheory
+
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+
+infixr:26 " ⥤ " => Functor
+
+namespace Functor
+
+section
+
+variable (C : Type u₁) [Category.{v₁} C]
+
+protected def id : C ⥤ C where
+  obj X := X
+  map f := f
+
+notation "𝟭" => Functor.id
+
+variable {C}
+
+@[simp]
+theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl
+
+@[simp]
+theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl
+
+end
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {E : Type u₃} [Category.{v₃} E]
+
+def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
+  obj X := G.obj (F.obj X)
+  map f := G.map (F.map f)
+
+infixr:80 " ⋙ " => Functor.comp
+
+@[simp] theorem comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) :
+  (F ⋙ G).obj X = G.obj (F.obj X) := rfl
+
+@[simp]
+theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
+    (F ⋙ G).map f = G.map (F.map f) := rfl
+
+end Functor
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Functor.Basic
+
+section Mathlib.CategoryTheory.NatTrans
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+@[ext]
+structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
+  app : ∀ X : C, F.obj X ⟶ G.obj X
+  naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f
+
+protected def NatTrans.id (F : C ⥤ D) : NatTrans F F where
+  app X := 𝟙 (F.obj X)
+  naturality := sorry
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.NatTrans
+
+section Mathlib.CategoryTheory.Iso
+
+namespace CategoryTheory
+
+structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
+  hom : X ⟶ Y
+  inv : Y ⟶ X
+  hom_inv_id : hom ≫ inv = 𝟙 X
+  inv_hom_id : inv ≫ hom = 𝟙 Y
+
+infixr:10 " ≅ " => Iso
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Iso
+
+section Mathlib.CategoryTheory.Functor.Category
+
+namespace CategoryTheory
+
+variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+
+namespace Functor
+
+instance category : Category.{max u₁ v₂} (C ⥤ D) where
+  Hom F G := NatTrans F G
+  id F := NatTrans.id F
+  comp α β := sorry
+  id_comp := sorry
+  comp_id := sorry
+
+@[ext]
+theorem ext' {F G : C ⥤ D} {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w
+
+end Functor
+
+namespace NatTrans
+
+@[simp]
+theorem id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
+
+@[simp]
+theorem comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
+    (α ≫ β).app X = α.app X ≫ β.app X := sorry
+
+end NatTrans
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Functor.Category
+
+section Mathlib.CategoryTheory.Idempotents.Karoubi
+
+namespace CategoryTheory
+
+variable (C : Type _) [Category C]
+
+structure Karoubi where
+  X : C
+  p : X ⟶ X
+
+namespace Karoubi
+
+variable {C}
+
+structure Hom (P Q : Karoubi C) where
+  f : P.X ⟶ Q.X
+  comm : f = P.p ≫ f ≫ Q.p
+
+theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f := sorry
+
+theorem comp_p {P Q : Karoubi C} (f : Hom P Q) : f.f ≫ Q.p = f.f := sorry
+
+/-- The category structure on the karoubi envelope of a category. -/
+instance : Category (Karoubi C) where
+  Hom := Karoubi.Hom
+  id P := ⟨P.p, sorry⟩
+  comp f g := ⟨f.f ≫ g.f, sorry⟩
+  comp_id := sorry
+  id_comp := sorry
+
+@[simp]
+theorem hom_ext_iff {P Q : Karoubi C} {f g : P ⟶ Q} : f = g ↔ f.f = g.f := sorry
+
+@[ext]
+theorem hom_ext {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g := sorry
+
+@[simp]
+theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f.f ≫ g.f := rfl
+
+@[simp]
+theorem id_f {P : Karoubi C} : Hom.f (𝟙 P) = P.p := rfl
+
+end Karoubi
+
+def toKaroubi : C ⥤ Karoubi C where
+  obj X := ⟨X, 𝟙 X⟩
+  map f := ⟨f, sorry⟩
+
+@[simp] theorem toKaroubi_obj_X (X : C) : ((toKaroubi C).obj X).X = X := rfl
+@[simp] theorem toKaroubi_obj_p (X : C) : ((toKaroubi C).obj X).p = 𝟙 X := rfl
+@[simp] theorem toKaroubi_map_f {X Y : C} (f : X ⟶ Y) : ((toKaroubi C).map f).f = f := rfl
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Idempotents.Karoubi
+
+section Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
+
+open CategoryTheory.Category
+open CategoryTheory.Karoubi
+
+namespace CategoryTheory
+namespace Idempotents
+
+variable (C : Type _) [Category C]
+
+theorem idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := sorry
+
+theorem p_comm_f {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) : P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f := sorry
+
+def inverse : Karoubi (Karoubi C) ⥤ Karoubi C where
+  obj P := ⟨P.X.X, P.p.f⟩
+  map f := ⟨f.f.f, sorry⟩
+
+theorem inverse_obj_X (P : Karoubi (Karoubi C)) : ((inverse C).obj P).X = P.X.X := rfl
+theorem inverse_obj_p (P : Karoubi (Karoubi C)) : ((inverse C).obj P).p = P.p.f := rfl
+theorem inverse_map_f {X Y : Karoubi (Karoubi C)} (f : X ⟶ Y) : ((inverse C).map f).f = f.f.f := rfl
+
+-- In the original source this is just
+-- ```
+-- def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where
+--   hom := { app := fun P => { f := { f := P.p.1 } } }
+--   inv := { app := fun P => { f := { f := P.p.1 }  } }
+-- ```
+-- but I've maximally expanded out the autoparams:
+-- it seems the slow down is in the `simp only` tactics, not the automation that finds them.
+
+def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where
+  hom :=
+    { app := fun P =>
+        { f :=
+            { f := P.p.1
+              comm := by simp only [Functor.comp_obj, toKaroubi_obj_X, inverse_obj_X,
+                Functor.id_obj, inverse_obj_p, comp_p, idem_f] }
+          comm := by simp only [Functor.comp_obj, toKaroubi_obj_X, Functor.id_obj, toKaroubi_obj_p,
+            Karoubi.id_f, inverse_obj_p, hom_ext_iff, inverse_obj_X, comp_f, idem_f] }
+      naturality := by
+        intro X Y f
+        simp only [Functor.comp_obj, Functor.id_obj, Functor.comp_map, toKaroubi_obj_X,
+          Functor.id_map, hom_ext_iff, comp_f, toKaroubi_map_f, inverse_obj_X, inverse_map_f,
+          p_comm_f] }
+  inv :=
+    { app := fun P =>
+        { f :=
+            { f := P.p.1
+              comm := by simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X,
+                inverse_obj_X, inverse_obj_p, idem_f, p_comp] }
+          comm := by simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X, toKaroubi_obj_p,
+            Karoubi.id_f, inverse_obj_p, hom_ext_iff, inverse_obj_X, comp_f, idem_f] }
+      naturality := by
+        intro X Y f
+        simp only [Functor.id_obj, Functor.comp_obj, Functor.id_map, toKaroubi_obj_X,
+          Functor.comp_map, hom_ext_iff, comp_f, toKaroubi_map_f, inverse_obj_X, inverse_map_f,
+          p_comm_f]
+    }
+  hom_inv_id := by
+    simp only [Functor.comp_obj, Functor.id_obj, toKaroubi_obj_X]
+    ext x : 4
+    simp only [Functor.comp_obj, toKaroubi_obj_X, inverse_obj_X, NatTrans.comp_app,
+      Functor.id_obj, comp_f, idem_f, NatTrans.id_app, Karoubi.id_f, toKaroubi_obj_p,
+      inverse_obj_p]
+  inv_hom_id := by
+    simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X]
+    ext x : 4
+    simp only [Functor.id_obj, NatTrans.comp_app, Functor.comp_obj, comp_f, toKaroubi_obj_X,
+      inverse_obj_X, idem_f, NatTrans.id_app, Karoubi.id_f]

From 26a336820bea75ae2f84716b8f2c1c1f874fcb35 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 29 Nov 2024 13:35:40 +1100
Subject: [PATCH 10/13] chore: add test for split

---
 tests/lean/run/4595_split.lean | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 tests/lean/run/4595_split.lean

diff --git a/tests/lean/run/4595_split.lean b/tests/lean/run/4595_split.lean
new file mode 100644
index 000000000000..e934e1157290
--- /dev/null
+++ b/tests/lean/run/4595_split.lean
@@ -0,0 +1,2 @@
+example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} : (if P then f else g) x = 37 := by
+  split <;> sorry

From 165fb2da8d6ec2c54301532ddf600f4b151ceedf Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 29 Nov 2024 14:17:03 +1100
Subject: [PATCH 11/13] chore: fix for FindSplitImpl.visit.visitApp?

---
 src/Lean/Meta/Tactic/SplitIf.lean | 31 +++++++++++++++----------------
 tests/lean/run/4595_split.lean    |  2 ++
 2 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 97489f9560a5..beb8981f39c8 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -61,24 +61,23 @@ unsafe def visit (e : Expr) : OptionT FindM Expr := do
     | .mdata _ b       => visit b
     | .forallE _ d b _ => visit d <|> visit b -- We want to look for candidates at `A → B`
     | .letE _ _ v b _  => visit v <|> visit b
-    | .app ..          => visitApp? e
+    | .app f a         => visitApp? f a
     | _                => failure
 where
-  visitApp? (e : Expr) : FindM (Option Expr) :=
-    e.withApp fun f args => do
-    let info ← getFunInfo f
-    for u : i in [0:args.size] do
-      let arg := args[i]
-      if h : i < info.paramInfo.size then
-        let info := info.paramInfo[i]
-        unless info.isProp do
-          if info.isExplicit then
-            let some found ← visit arg | pure ()
-            return found
-      else
-        let some found ← visit arg | pure ()
-        return found
-    visit f
+  visitApp? (f a : Expr) : FindM (Option Expr) := do
+    if let some found ← visit f then
+      return found
+    let info ← getFunInfoNArgs f 1
+    if h : 0 < info.paramInfo.size then
+      let info := info.paramInfo[0]
+      unless info.isProp do
+        if info.isExplicit then
+          let some found ← visit a | pure ()
+          return found
+    else
+      let some found ← visit a | pure ()
+      return found
+    return none
 
 end FindSplitImpl
 
diff --git a/tests/lean/run/4595_split.lean b/tests/lean/run/4595_split.lean
index e934e1157290..19e0d949b82b 100644
--- a/tests/lean/run/4595_split.lean
+++ b/tests/lean/run/4595_split.lean
@@ -1,2 +1,4 @@
+set_option trace.split.debug true
+
 example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} : (if P then f else g) x = 37 := by
   split <;> sorry

From 204817295027291efb8669c7820d5ce4cbccf896 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 29 Nov 2024 16:53:11 +1100
Subject: [PATCH 12/13] check for loose bvars

---
 src/Lean/Meta/Tactic/SplitIf.lean | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index beb8981f39c8..6c1d88ad73ef 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -67,17 +67,21 @@ where
   visitApp? (f a : Expr) : FindM (Option Expr) := do
     if let some found ← visit f then
       return found
-    let info ← getFunInfoNArgs f 1
-    if h : 0 < info.paramInfo.size then
-      let info := info.paramInfo[0]
-      unless info.isProp do
-        if info.isExplicit then
-          let some found ← visit a | pure ()
-          return found
+    if f.hasLooseBVars then
+      -- `getFunInfo` may fail, so we just visit all arguments.
+      visit a
     else
-      let some found ← visit a | pure ()
-      return found
-    return none
+      let info ← getFunInfoNArgs f 1
+      if h : 0 < info.paramInfo.size then
+        let info := info.paramInfo[0]
+        unless info.isProp do
+          if info.isExplicit then
+            let some found ← visit a | pure ()
+            return found
+      else
+        let some found ← visit a | pure ()
+        return found
+      return none
 
 end FindSplitImpl
 

From 28b51413fc5cb850c4d23f94b5a2ee5d5988ac8e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 29 Nov 2024 12:36:08 -0800
Subject: [PATCH 13/13] chore: ensures `getFunInfo` is used effectively

We want to overhead of processing every single partial application.
---
 src/Lean/Meta/Tactic/SplitIf.lean | 55 ++++++++++++++++++-------------
 tests/lean/run/4595_split.lean    | 15 +++++++--
 2 files changed, 45 insertions(+), 25 deletions(-)

diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
index 6c1d88ad73ef..b6734f21571f 100644
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -28,19 +28,28 @@ structure Context where
 
 unsafe abbrev FindM := ReaderT Context $ StateT (PtrSet Expr) MetaM
 
-private def isCandidate (env : Environment) (ctx : Context) (e : Expr) : Bool := Id.run do
-  if ctx.exceptionSet.contains e then
-    return false
-  if ctx.kind.considerIte && (e.isIte || e.isDIte) then
-    return !(e.getArg! 1 5).hasLooseBVars
+/--
+Checks whether `e` is a candidate for `split`.
+Returns `some e'` if a prefix is a candidate.
+Example: suppose `e` is `(if b then f else g) x`, then
+the result is `some e'` where `e'` is the subterm `(if b then f else g)`
+-/
+private def isCandidate? (env : Environment) (ctx : Context) (e : Expr) : Option Expr := Id.run do
+  let ret (e : Expr) : Option Expr :=
+    if ctx.exceptionSet.contains e then none else some e
+  if ctx.kind.considerIte then
+    if e.isAppOf ``ite || e.isAppOf ``dite then
+      let numArgs := e.getAppNumArgs
+      if numArgs >= 5 && !(e.getArg! 1 5).hasLooseBVars then
+        return ret (e.getBoundedAppFn (numArgs - 5))
   if ctx.kind.considerMatch then
     if let some info := isMatcherAppCore? env e then
       let args := e.getAppArgs
       for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
         if args[i]!.hasLooseBVars then
-          return false
-      return true
-  return false
+          return none
+      return ret (e.getBoundedAppFn (args.size - info.arity))
+  return none
 
 @[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
   if (← get).contains e then
@@ -49,7 +58,7 @@ private def isCandidate (env : Environment) (ctx : Context) (e : Expr) : Bool :=
 
 unsafe def visit (e : Expr) : OptionT FindM Expr := do
   checkVisited e
-  if isCandidate (← getEnv) (← read) e then
+  if let some e := isCandidate? (← getEnv) (← read) e then
     return e
   else
     -- We do not look for split candidates in proofs.
@@ -61,27 +70,29 @@ unsafe def visit (e : Expr) : OptionT FindM Expr := do
     | .mdata _ b       => visit b
     | .forallE _ d b _ => visit d <|> visit b -- We want to look for candidates at `A → B`
     | .letE _ _ v b _  => visit v <|> visit b
-    | .app f a         => visitApp? f a
+    | .app ..          => visitApp? e
     | _                => failure
 where
-  visitApp? (f a : Expr) : FindM (Option Expr) := do
-    if let some found ← visit f then
-      return found
-    if f.hasLooseBVars then
-      -- `getFunInfo` may fail, so we just visit all arguments.
-      visit a
+  visitApp? (e : Expr) : FindM (Option Expr) :=
+    e.withApp fun f args => do
+    -- See comment at `Canonicalizer.lean` regarding the case where
+    -- `f` has loose bound variables.
+    let info ← if f.hasLooseBVars then
+      pure {}
     else
-      let info ← getFunInfoNArgs f 1
-      if h : 0 < info.paramInfo.size then
-        let info := info.paramInfo[0]
+      getFunInfo f
+    for u : i in [0:args.size] do
+      let arg := args[i]
+      if h : i < info.paramInfo.size then
+        let info := info.paramInfo[i]
         unless info.isProp do
           if info.isExplicit then
-            let some found ← visit a | pure ()
+            let some found ← visit arg | pure ()
             return found
       else
-        let some found ← visit a | pure ()
+        let some found ← visit arg | pure ()
         return found
-      return none
+    visit f
 
 end FindSplitImpl
 
diff --git a/tests/lean/run/4595_split.lean b/tests/lean/run/4595_split.lean
index 19e0d949b82b..f97399921217 100644
--- a/tests/lean/run/4595_split.lean
+++ b/tests/lean/run/4595_split.lean
@@ -1,4 +1,13 @@
-set_option trace.split.debug true
-
 example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} : (if P then f else g) x = 37 := by
-  split <;> sorry
+  split
+  · guard_target =ₛ  f x = 37
+    sorry
+  · guard_target =ₛ  g x = 37
+    sorry
+
+example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} {b : Bool} : (match b with | true => f | false => g) x = 37 := by
+  split
+  · guard_target =ₛ  f x = 37
+    sorry
+  · guard_target =ₛ  g x = 37
+    sorry