diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index 5c31c1a7384b..e1230973c369 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/src/Lean/Meta/Tactic/Grind/Core.lean
@@ -106,6 +106,15 @@ private def closeGoalWithTrueEqFalse : GoalM Unit := do
     let falseProof ← mkEqMP trueEqFalse (mkConst ``True.intro)
     closeGoal falseProof
 
+/-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class. -/
+private def closeGoalWithValuesEq (lhs rhs : Expr) : GoalM Unit := do
+  let p ← mkEq lhs rhs
+  let hp ← mkEqProof lhs rhs
+  let d ← mkDecide p
+  let pEqFalse := mkApp3 (mkConst ``eq_false_of_decide) p d.appArg! (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``false))
+  let falseProof ← mkEqMP pEqFalse hp
+  closeGoal falseProof
+
 private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   trace[grind.eq] "{lhs} {if isHEq then "≡" else "="} {rhs}"
   let lhsNode ← getENode lhs
@@ -119,8 +128,8 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   let mut valueInconsistency := false
   let mut trueEqFalse := false
   if lhsRoot.interpreted && rhsRoot.interpreted then
-    markAsInconsistent
     if lhsNode.root.isTrue || rhsNode.root.isTrue then
+      markAsInconsistent
       trueEqFalse := true
     else
       valueInconsistency := true
@@ -135,7 +144,9 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   unless (← isInconsistent) do
     if lhsRoot.ctor && rhsRoot.ctor then
       propagateCtor lhsRoot.self rhsRoot.self
-  -- TODO: propagate value inconsistency
+  unless (← isInconsistent) do
+    if valueInconsistency then
+      closeGoalWithValuesEq lhsRoot.self rhsRoot.self
   trace[grind.debug] "after addEqStep, {← ppState}"
   checkInvariants
 where
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 0230896a3883..0d4b9ada9813 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -34,3 +34,24 @@ example (h : x = y) (h₁ : a :: b = x) (h₂ : c :: d = y) : b = d := by
 
 example (a b : Sum Nat Bool) : a = .inl x → b = .inl y → x ≠ y → a = b → False := by
   grind
+
+example (a b : Nat) : a = 1 → b = 2 → a = b → False := by
+  grind
+
+example (a b c : Int) : a = 1 → c = -2 → a = b → c = b → False := by
+  grind
+
+example (a b : Char) : a = 'h' → b = 'w' → a = b → False := by
+  grind
+
+example (a b : String) : a = "hello" → b = "world" → a = b → False := by
+  grind
+
+example (a b c : String) : a = c → a = "hello" → c = "world" → c = b → False := by
+  grind
+
+example (a b c : BitVec 32) : a = c → a = 1#32 → c = 2#32 → c = b → False := by
+  grind
+
+example (a b c : UInt32) : a = c → a = 1 → c = 200 → c = b → False := by
+  grind