diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 1e40f7fc6d..219b1c73f7 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -211,6 +211,10 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
         let c := args[0]!
         internalize c generation e
         registerParent e c
+      else if f.isConstOf ``ite && args.size == 5 then
+        let c := args[1]!
+        internalize c generation e
+        registerParent e c
       else
         if let .const fName _ := f then
           activateTheoremPatterns fName generation
diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index be6cab0a24..47fd8f805e 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -171,8 +171,10 @@ builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
 builtin_grind_propagator propagateIte ↑ite := fun e => do
   let_expr f@ite α c h a b := e | return ()
   if (← isEqTrue c) then
+    internalize a (← getGeneration e)
     pushEq e a <| mkApp6 (mkConst ``ite_cond_eq_true f.constLevels!) α c h a b (← mkEqTrueProof c)
   else if (← isEqFalse c) then
+    internalize b (← getGeneration e)
     pushEq e b <| mkApp6 (mkConst ``ite_cond_eq_false f.constLevels!) α c h a b (← mkEqFalseProof c)
 
 /-- Propagates `dite` upwards -/
diff --git a/tests/lean/run/grind_lazy_ite.lean b/tests/lean/run/grind_lazy_ite.lean
new file mode 100644
index 0000000000..d7571794ba
--- /dev/null
+++ b/tests/lean/run/grind_lazy_ite.lean
@@ -0,0 +1,24 @@
+def f (n : Nat) (m : Nat) :=
+  if n < m then
+    f (n+1) m + n
+  else
+    n
+
+/--
+info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example : f 5 m > 0 := by
+  fail_if_success grind (splits := 0) [f.eq_def]
+  sorry
+
+/--
+info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5
+[grind.ematch.instance] f.eq_def: f 6 m = if 6 < m then f (6 + 1) m + 6 else 6
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example : f 5 m > 0 := by
+  fail_if_success grind (splits := 1) [f.eq_def]
+  sorry