diff --git a/tests/lean/grind/algebra/omega.lean b/tests/lean/grind/algebra/omega.lean
index f2205e03c6..48ae0d7b26 100644
--- a/tests/lean/grind/algebra/omega.lean
+++ b/tests/lean/grind/algebra/omega.lean
@@ -1,3 +1,34 @@
+-- From Mathlib.Algebra.Order.Group.Unbundled.Int
+class SubNegMonoid (G : Type u) extends Neg G where
+
+instance Int.instSubNegMonoid : SubNegMonoid Int where
+
+theorem Int.abs_sub_lt_of_lt_lt.extracted_1_1 {m a b : Nat} {m a b : Nat} (ha : a < m) (hb : b < m) :
+    (@Neg.neg Int
+      (Int.instSubNegMonoid.toNeg)
+      (m : Int)) < (↑b - ↑a) ∧
+    (↑b - ↑a < ↑m) := by
+  grind
+
+-- From Mathlib.Order.RelSeries
+theorem RelSeries.inductionOn.extracted_3 (p : Nat) (heq : p = 0) (n : Fin (p + 1)) : n = 0 := by
+  grind
+
+theorem LTSeries.length_lt_card.extracted_1 (s : Nat)
+  (i j : Fin (s + 1)) (hn : i ≠ j) (hl : ¬i < j) : j < i := by
+  grind
+
+-- From Mathlib.AlgebraicTopology.SimplexCategory.Basic
+theorem SimplexCategory.mkOfLe_refl.extracted_1 {n : Nat} (j : Fin (n + 1)) : j ≤ j := by
+  grind
+
+theorem SimplexCategory.eq_σ_comp_of_not_injective.extracted_1 {n : Nat}
+  (x y : Fin ((n + 1) + 1)) (h₂ : ¬x = y) (h : ¬x < y) :
+  y < x := by
+  fail_if_success grind
+  omega
+
+
 -- Comparisons against `omega`:
 -- set_option diagnostics true
 -- This one is much slower (~10s in the kernel) than omega (~2s in the kernel).