diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean
index 5672b5618d..b19515b7e6 100644
--- a/src/Init/Grind/Lemmas.lean
+++ b/src/Init/Grind/Lemmas.lean
@@ -25,6 +25,9 @@ theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = Fals
 theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True := by simp_all
 theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True := by simp_all
 
+theorem or_of_and_eq_false {a b : Prop} (h : (a ∧ b) = False) : (¬a ∨ ¬b) := by
+  by_cases a <;> by_cases b <;> simp_all
+
 /-! Or -/
 
 theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True := by simp [h]
diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 7def9222d4..3696eca31c 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -24,14 +24,9 @@ The configuration for `grind`.
 Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
 -/
 structure Config where
-  /-- When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match` expressions during internalization. -/
-  eager : Bool := false
-  /-- Maximum number of branches (i.e., case-splits) in the proof search tree. -/
-  splits : Nat := 100
-  /--
-  Maximum number of E-matching (aka heuristic theorem instantiation)
-  in a proof search tree branch.
-  -/
+  /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
+  splits : Nat := 5
+  /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--
   Maximum term generation.
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index 022695fb35..593bb147c6 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -39,6 +39,9 @@ builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
+builtin_initialize registerTraceClass `grind.split
+builtin_initialize registerTraceClass `grind.split.candidate
+builtin_initialize registerTraceClass `grind.split.resolved
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
diff --git a/src/Lean/Meta/Tactic/Grind/Combinators.lean b/src/Lean/Meta/Tactic/Grind/Combinators.lean
new file mode 100644
index 0000000000..cfeb0efb2a
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Combinators.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+/-!
+Combinators for manipulating `GrindTactic`s.
+TODO: a proper tactic language for `grind`.
+-/
+
+def GrindTactic := Goal → GrindM (Option (List Goal))
+
+def GrindTactic.try (x : GrindTactic) : GrindTactic := fun g => do
+  let some gs ← x g | return some [g]
+  return some gs
+
+def applyToAll (x : GrindTactic)  (goals : List Goal) : GrindM (List Goal) := do
+  go goals []
+where
+  go (goals : List Goal) (acc : List Goal) : GrindM (List Goal) := do
+    match goals with
+    | [] => return acc.reverse
+    | goal :: goals => match (← x goal) with
+      | none => go goals (goal :: acc)
+      | some goals' => go goals (goals' ++ acc)
+
+partial def GrindTactic.andThen (x y : GrindTactic) : GrindTactic := fun goal => do
+  let some goals ← x goal | return none
+  applyToAll y goals
+
+instance : AndThen GrindTactic where
+  andThen a b := GrindTactic.andThen a (b ())
+
+partial def GrindTactic.iterate (x : GrindTactic) : GrindTactic := fun goal => do
+  go [goal] []
+where
+  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
+    match todo with
+    | [] => return result
+    | goal :: todo =>
+      if let some goalsNew ← x goal then
+        go (goalsNew ++ todo) result
+      else
+        go todo (goal :: result)
+
+partial def GrindTactic.orElse (x y : GrindTactic) : GrindTactic := fun goal => do
+  let some goals ← x goal | y goal
+  return goals
+
+instance : OrElse GrindTactic where
+  orElse a b := GrindTactic.andThen a (b ())
+
+def toGrindTactic (f : GoalM Unit) : GrindTactic := fun goal => do
+  let goal ← GoalM.run' goal f
+  if goal.inconsistent then
+    return some []
+  else
+    return some [goal]
+
+def GrindTactic' := Goal → GrindM (List Goal)
+
+def GrindTactic'.toGrindTactic (x : GrindTactic') : GrindTactic := fun goal => do
+  let goals ← x goal
+  return some goals
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 64b716c698..4ba4d6eff9 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -51,6 +51,8 @@ structure Context where
   useMT : Bool := true
   /-- `EMatchTheorem` being processed. -/
   thm   : EMatchTheorem := default
+  /-- Initial application used to start E-matching -/
+  initApp : Expr := default
   deriving Inhabited
 
 /-- State for the E-matching monad -/
@@ -64,6 +66,9 @@ abbrev M := ReaderT Context $ StateRefT State GoalM
 def M.run' (x : M α) : GoalM α :=
   x {} |>.run' {}
 
+@[inline] private abbrev withInitApp (e : Expr) (x : M α) : M α :=
+  withReader (fun ctx => { ctx with initApp := e }) x
+
 /--
 Assigns `bidx := e` in `c`. If `bidx` is already assigned in `c`, we check whether
 `e` and `c.assignment[bidx]` are in the same equivalence class.
@@ -213,6 +218,8 @@ private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) :
     check proof
   let mut prop ← inferType proof
   if Match.isMatchEqnTheorem (← getEnv) origin.key then
+    -- `initApp` is a match-application that we don't need to split at anymore.
+    markCaseSplitAsResolved (← read).initApp
     prop ← annotateMatchEqnType prop
   trace[grind.ematch.instance] "{← origin.pp}: {prop}"
   addTheoremInstance proof prop (generation+1)
@@ -288,9 +295,10 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
     let n ← getENode app
     if (n.heqProofs || n.isCongrRoot) &&
        (!useMT || n.mt == gmt) then
-      if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
-        modify fun s => { s with choiceStack := [c] }
-        processChoices
+      withInitApp app do
+        if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
+          modify fun s => { s with choiceStack := [c] }
+          processChoices
 
 def ematchTheorem (thm : EMatchTheorem) : M Unit := do
   if (← checkMaxInstancesExceeded) then return ()
@@ -341,14 +349,14 @@ def ematch : GoalM Unit := do
     }
 
 /-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert? (goal : Goal) : GrindM (Option (List Goal)) := do
+def ematchAndAssert : GrindTactic := fun goal => do
   let numInstances := goal.numInstances
   let goal ← GoalM.run' goal ematch
   if goal.numInstances == numInstances then
     return none
   assertAll goal
 
-def ematchStar (goal : Goal) : GrindM (List Goal) := do
-  iterate goal ematchAndAssert?
+def ematchStar : GrindTactic :=
+  ematchAndAssert.iterate
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index fe801763f3..75b4743033 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -31,6 +31,10 @@ def addCongrTable (e : Expr) : GoalM Unit := do
   else
     modify fun s => { s with congrTable := s.congrTable.insert { e } }
 
+/--
+Given an application `e` of the form `f a_1 ... a_n`,
+adds entry `f ↦ e` to `appMap`. Recall that `appMap` is a multi-map.
+-/
 private def updateAppMap (e : Expr) : GoalM Unit := do
   let key := e.toHeadIndex
   modify fun s => { s with
@@ -40,6 +44,34 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
       s.appMap.insert key [e]
   }
 
+/-- Inserts `e` into the list of case-split candidates. -/
+private def addSplitCandidate (e : Expr) : GoalM Unit := do
+  trace[grind.split.candidate] "{e}"
+  modify fun s => { s with splitCadidates := e :: s.splitCadidates }
+
+-- TODO: add attribute to make this extensible
+private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
+
+/-- Inserts `e` into the list of case-split candidates if applicable. -/
+private def checkAndaddSplitCandidate (e : Expr) : GoalM Unit := do
+  unless e.isApp do return ()
+  if e.isIte || e.isDIte then
+    addSplitCandidate e
+  else if (← isMatcherApp e) then
+    if let .reduced _ ← reduceMatcher? e then
+      -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
+      -- and consequently don't need to be splitted.
+      return ()
+    else
+      addSplitCandidate e
+  else
+    let .const declName _  := e.getAppFn | return ()
+    if forbiddenSplitTypes.contains declName then return ()
+    -- We should have a mechanism for letting users to select types to case-split.
+    -- Right now, we just consider inductive predicates that are not in the forbidden list
+    if (← isInductivePredicate declName) then
+      addSplitCandidate e
+
 mutual
 /-- Internalizes the nested ground terms in the given pattern. -/
 private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
@@ -116,6 +148,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       -- We do not want to internalize the components of a literal value.
       mkENode e generation
     else e.withApp fun f args => do
+      checkAndaddSplitCandidate e
       addMatchEqns f generation
       if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
         -- We only internalize the proposition. We can skip the proof because of
diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean
index 3923b4d1ab..1fa58b4a60 100644
--- a/src/Lean/Meta/Tactic/Grind/Intro.lean
+++ b/src/Lean/Meta/Tactic/Grind/Intro.lean
@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Combinators
 
 namespace Lean.Meta.Grind
 
@@ -88,7 +89,7 @@ private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal
     return none
 
 /-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
-partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
+partial def intros  (generation : Nat) : GrindTactic' := fun goal => do
   let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
     if goal.inconsistent then
       return ()
@@ -116,11 +117,11 @@ partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
   return goals.toList
 
 /-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
-def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : GrindM (List Goal) := do
+def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : GrindTactic' := fun goal => do
   if (← isCasesCandidate prop) then
     let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
     let goal := { goal with mvarId }
-    intros goal generation
+    intros generation goal
   else
     let goal ← GoalM.run' goal do
       let r ← simp prop
@@ -130,25 +131,13 @@ def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : Gri
     if goal.inconsistent then return [] else return [goal]
 
 /-- Asserts next fact in the `goal` fact queue. -/
-def assertNext? (goal : Goal) : GrindM (Option (List Goal)) := do
+def assertNext : GrindTactic := fun goal => do
   let some (fact, newFacts) := goal.newFacts.dequeue?
     | return none
-  assertAt { goal with newFacts } fact.proof fact.prop fact.generation
-
-partial def iterate (goal : Goal) (f : Goal → GrindM (Option (List Goal))) : GrindM (List Goal) := do
-  go [goal] []
-where
-  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
-    match todo with
-    | [] => return result
-    | goal :: todo =>
-      if let some goalsNew ← f goal then
-        go (goalsNew ++ todo) result
-      else
-        go todo (goal :: result)
+  assertAt fact.proof fact.prop fact.generation { goal with newFacts }
 
 /-- Asserts all facts in the `goal` fact queue. -/
-partial def assertAll (goal : Goal) : GrindM (List Goal) := do
-  iterate goal assertNext?
+partial def assertAll : GrindTactic :=
+  assertNext.iterate
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean
index 139b32eceb..60a8fa0e95 100644
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.SimpUtil
 
 namespace Lean.Meta.Grind
@@ -68,7 +69,7 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
 
 /-- A very simple strategy -/
 private def simple (goals : List Goal) : GrindM (List Goal) := do
-  all goals ematchStar
+  applyToAll (ematchStar >> (splitNext >> ematchStar).iterate) goals
 
 def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
   let go : GrindM (List MVarId) := do
diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
new file mode 100644
index 0000000000..7c98474232
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.Cases
+
+namespace Lean.Meta.Grind
+
+inductive CaseSplitStatus where
+  | resolved
+  | notReady
+  | ready
+  deriving Inhabited, BEq
+
+private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
+  match_expr e with
+  | Or a b =>
+    if (← isEqTrue e) then
+      if (← isEqTrue a <||> isEqTrue b) then
+        return .resolved
+      else
+        return .ready
+    else if (← isEqFalse e) then
+      return .resolved
+    else
+      return .notReady
+  | And a b =>
+    if (← isEqTrue e) then
+      return .resolved
+    else if (← isEqFalse e) then
+      if (← isEqFalse a <||> isEqFalse b) then
+        return .resolved
+      else
+        return .ready
+    else
+      return .notReady
+  | ite _ c _ _ _ =>
+    if (← isEqTrue c <||> isEqFalse c) then
+      return .resolved
+    else
+      return .ready
+  | dite _ c _ _ _ =>
+    if (← isEqTrue c <||> isEqFalse c) then
+      return .resolved
+    else
+      return .ready
+  | _ =>
+    if (← isResolvedCaseSplit e) then
+      return .resolved
+    if (← isMatcherApp e) then
+      return .notReady -- TODO: implement splittes for `match`
+      -- return .ready
+    let .const declName .. := e.getAppFn | unreachable!
+    if (← isInductivePredicate declName <&&> isEqTrue e) then
+      return .ready
+    return .notReady
+
+/-- Returns the next case-split to be peformed. It uses a very simple heuristic. -/
+private def selectNextSplit? : GoalM (Option Expr) := do
+  if (← isInconsistent) then return none
+  if (← checkMaxCaseSplit) then return none
+  go (← get).splitCadidates none []
+where
+  go (cs : List Expr) (c? : Option Expr) (cs' : List Expr) : GoalM (Option Expr) := do
+    match cs with
+    | [] =>
+      modify fun s => { s with splitCadidates := cs'.reverse }
+      if c?.isSome then
+        -- Remark: we reset `numEmatch` after each case split.
+        -- We should consider other strategies in the future.
+        modify fun s => { s with numSplits := s.numSplits + 1, numEmatch := 0 }
+      return c?
+    | c::cs =>
+    match (← checkCaseSplitStatus c) with
+    | .notReady => go cs c? (c::cs')
+    | .resolved => go cs c? cs'
+    | .ready =>
+    match c? with
+    | none => go cs (some c) cs'
+    | some c' =>
+      if (← getGeneration c) < (← getGeneration c') then
+        go cs (some c) (c'::cs')
+      else
+        go cs c? (c::cs')
+
+/-- Constructs a major premise for the `cases` tactic used by `grind`. -/
+private def mkCasesMajor (c : Expr) : GoalM Expr := do
+  match_expr c with
+  | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
+  | ite _ c _ _ _ => return mkEM c
+  | dite _ c _ _ _ => return mkEM c
+  | _ => return mkApp2 (mkConst ``of_eq_true) c (← mkEqTrueProof c)
+
+/-- Introduces new hypotheses in each goal. -/
+private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do
+  match goals with
+  | [] => return acc.reverse
+  | goal::goals => introNewHyp goals ((← intros generation goal) ++ acc) generation
+
+/--
+Selects a case-split from the list of candidates,
+and returns a new list of goals if successful.
+-/
+def splitNext : GrindTactic := fun goal => do
+  let (goals?, _) ← GoalM.run goal do
+    let some c ← selectNextSplit?
+      | return none
+    let gen ← getGeneration c
+    trace[grind.split] "{c}, generation: {gen}"
+    -- TODO: `match`
+    let major ← mkCasesMajor c
+    let mvarIds ← cases (← get).mvarId major
+    let goal ← get
+    let goals := mvarIds.map fun mvarId => { goal with mvarId }
+    let goals ← introNewHyp goals [] (gen+1)
+    return some goals
+  return goals?
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 80b934fc18..4544196da5 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -374,8 +374,7 @@ structure Goal where
   thmMap       : EMatchTheorems
   /-- Number of theorem instances generated so far -/
   numInstances : Nat := 0
-  /-- Number of E-matching rounds performed in this goal so far. -/
-  -- Remark: it is always equal to `gmt` in the current implementation.
+  /-- Number of E-matching rounds performed in this goal since the last case-split. -/
   numEmatch    : Nat := 0
   /-- (pre-)instances found so far. It includes instances that failed to be instantiated. -/
   preInstances : PreInstanceSet := {}
@@ -383,6 +382,12 @@ structure Goal where
   newFacts     : Std.Queue NewFact := ∅
   /-- `match` auxiliary functions whose equations have already been created and activated. -/
   matchEqNames : PHashSet Name := {}
+  /-- Case-split candidates. -/
+  splitCadidates : List Expr := []
+  /-- Number of splits performed to get to this goal. -/
+  numSplits : Nat := 0
+  /-- Case-splits that do not have to be performed anymore. -/
+  resolvedSplits : PHashSet ENodeKey := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -420,6 +425,10 @@ def addTheoremInstance (proof : Expr) (prop : Expr) (generation : Nat) : GoalM U
 def checkMaxInstancesExceeded : GoalM Bool := do
   return (← get).numInstances >= (← getConfig).instances
 
+/-- Returns `true` if the maximum number of case-splits has been reached. -/
+def checkMaxCaseSplit : GoalM Bool := do
+  return (← get).numSplits >= (← getConfig).splits
+
 /-- Returns `true` if the maximum number of E-matching rounds has been reached. -/
 def checkMaxEmatchExceeded : GoalM Bool := do
   return (← get).numEmatch >= (← getConfig).ematch
@@ -732,4 +741,17 @@ partial def getEqcs : GoalM (List (List Expr)) := do
       r := (← getEqc node.self) :: r
   return r
 
+/-- Returns `true` if `e` is a case-split that does not need to be performed anymore. -/
+def isResolvedCaseSplit (e : Expr) : GoalM Bool :=
+  return (← get).resolvedSplits.contains { expr := e }
+
+/--
+Mark `e` as a case-split that does not need to be performed anymore.
+Remark: we currently use this feature to disable `match`-case-splits
+-/
+def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
+  unless (← isResolvedCaseSplit e) do
+    trace[grind.split.resolved] "{e}"
+    modify fun s => { s with resolvedSplits := s.resolvedSplits.insert { expr := e } }
+
 end Lean.Meta.Grind
diff --git a/tests/lean/run/grind_implies.lean b/tests/lean/run/grind_implies.lean
new file mode 100644
index 0000000000..9e68cc2e55
--- /dev/null
+++ b/tests/lean/run/grind_implies.lean
@@ -0,0 +1,87 @@
+set_option trace.grind.eqc true
+set_option trace.grind.internalize true
+
+/--
+info: [grind.internalize] p → q
+[grind.internalize] p
+[grind.internalize] q
+[grind.eqc] (p → q) = True
+[grind.eqc] p = True
+[grind.eqc] (p → q) = q
+[grind.eqc] q = False
+-/
+#guard_msgs (info) in
+example (p q : Prop) : (p → q) → p → q := by
+  grind
+
+/--
+info: [grind.internalize] p → q
+[grind.internalize] p
+[grind.internalize] q
+[grind.eqc] (p → q) = True
+[grind.eqc] q = False
+[grind.eqc] p = True
+[grind.eqc] (p → q) = q
+-/
+#guard_msgs (info) in
+example (p q : Prop) : (p → q) → ¬q → ¬p := by
+  grind
+
+/--
+info: [grind.internalize] p → q
+[grind.internalize] p
+[grind.internalize] q
+[grind.internalize] r
+[grind.eqc] (p → q) = r
+[grind.eqc] p = False
+[grind.eqc] (p → q) = True
+[grind.eqc] r = False
+-/
+#guard_msgs (info) in
+example (p q : Prop) : (p → q) = r → ¬p → r := by
+  grind
+
+
+/--
+info: [grind.internalize] p → q
+[grind.internalize] p
+[grind.internalize] q
+[grind.internalize] r
+[grind.eqc] (p → q) = r
+[grind.eqc] q = True
+[grind.eqc] (p → q) = True
+[grind.eqc] r = False
+-/
+#guard_msgs (info) in
+example (p q : Prop) : (p → q) = r → q → r := by
+  grind
+
+/--
+info: [grind.internalize] p → q
+[grind.internalize] p
+[grind.internalize] q
+[grind.internalize] r
+[grind.eqc] (p → q) = r
+[grind.eqc] q = False
+[grind.eqc] r = True
+[grind.eqc] p = True
+[grind.eqc] (p → q) = q
+-/
+#guard_msgs (info) in
+example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by
+  grind
+
+/--
+info: [grind.internalize] p → q
+[grind.internalize] p
+[grind.internalize] q
+[grind.internalize] r
+[grind.eqc] (p → q) = r
+[grind.eqc] q = False
+[grind.eqc] r = False
+[grind.eqc] p = True
+[grind.eqc] p = False
+-/
+#guard_msgs (info) in
+example (p q : Prop) : (p → q) = r → ¬q → ¬r → p := by
+  grind
diff --git a/tests/lean/run/grind_match1.lean b/tests/lean/run/grind_match1.lean
index 483b8600c0..c50bfcf6e6 100644
--- a/tests/lean/run/grind_match1.lean
+++ b/tests/lean/run/grind_match1.lean
@@ -7,6 +7,8 @@ def g (xs : List α) (ys : List α) :=
 attribute [simp] g
 
 set_option trace.grind.assert true
+set_option trace.grind.split.candidate true
+set_option trace.grind.split.resolved true
 
 /--
 info: [grind.assert] (match as, bs with
@@ -14,10 +16,18 @@ info: [grind.assert] (match as, bs with
       | head :: head_1 :: tail, [] => []
       | x :: xs, ys => x :: g xs ys) =
       d
+[grind.split.candidate] match as, bs with
+    | [], x => bs
+    | head :: head_1 :: tail, [] => []
+    | x :: xs, ys => x :: g xs ys
 [grind.assert] bs = []
 [grind.assert] a₁ :: f 0 = as
 [grind.assert] f 0 = a₂ :: f 1
 [grind.assert] ¬d = []
+[grind.split.resolved] match as, bs with
+    | [], x => bs
+    | head :: head_1 :: tail, [] => []
+    | x :: xs, ys => x :: g xs ys
 [grind.assert] (match a₁ :: a₂ :: f 1, [] with
       | [], x => bs
       | head :: head_1 :: tail, [] => []
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 63c247088b..be879cd202 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -12,6 +12,8 @@ right✝ : b = true ∨ c = true
 left : p
 right : q
 x✝ : b = false ∨ a = false
+h✝ : b = false
+h : c = true
 ⊢ False
 -/
 #guard_msgs (error) in
diff --git a/tests/lean/run/grind_split.lean b/tests/lean/run/grind_split.lean
new file mode 100644
index 0000000000..917e62e6b7
--- /dev/null
+++ b/tests/lean/run/grind_split.lean
@@ -0,0 +1,35 @@
+set_option trace.grind.split true
+set_option trace.grind.eqc true
+example (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
+  grind
+
+opaque R : Nat → Prop
+
+example (p : Prop) [Decidable p] (a b c : Nat) : (if p then a else b) = c → R a → R b → R c := by
+  grind
+
+
+namespace grind_test_induct_pred
+
+inductive Expr where
+  | nat  : Nat → Expr
+  | plus : Expr → Expr → Expr
+  | bool : Bool → Expr
+  | and  : Expr → Expr → Expr
+  deriving DecidableEq
+
+inductive Ty where
+  | nat
+  | bool
+  deriving DecidableEq
+
+inductive HasType : Expr → Ty → Prop
+  | nat  : HasType (.nat v) .nat
+  | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat
+  | bool : HasType (.bool v) .bool
+  | and  : HasType a .bool → HasType b .bool → HasType (.and a b) .bool
+
+theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
+  grind
+
+end grind_test_induct_pred