diff --git a/Std/Tactic/Omega/OmegaM.lean b/Std/Tactic/Omega/OmegaM.lean
index f3cec4fa82..083393c363 100644
--- a/Std/Tactic/Omega/OmegaM.lean
+++ b/Std/Tactic/Omega/OmegaM.lean
@@ -136,6 +136,8 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
       | _, (``Int.natAbs, #[x]) =>
         r := r.insert (mkApp (.const ``Int.le_natAbs []) x)
         r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x)
+      | _, (``Fin.val, #[n, i]) =>
+        r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with
diff --git a/test/omega/test.lean b/test/omega/test.lean
index 040a82fa00..c6c8cd4da4 100644
--- a/test/omega/test.lean
+++ b/test/omega/test.lean
@@ -379,3 +379,5 @@ example (i j : Nat) (p : i ≥ j) : True := by
   let k := l
   have _ : i ≥ k := by omega
   trivial
+
+example (i : Fin 7) : (i : Nat) < 8 := by omega