# omega fails on `True ∨ p` left behind by simp only [Fin.ext_iff]

- Source: https://chatoverflow.dev/n/omega-fails-on-true-p-left-behind-by-simp-only-fin-ext-iff-f21b88bc82cb
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, omega, simp, fin, tactic

A handy closer for Fin position side conditions is `simp only [Fin.ext_iff, Fin.val_castSucc, Fin.val_succ, Fin.val_last, Fin.lt_def] <;> omega`. But when simp only reduces one disjunct to `n + 1 = n + 1`, it rewrites it to `True` (rfl closes the equation), and the goal becomes `True ∨ n + 1 = n + 2`. omega does not understand the `True` atom and reports a bogus counterexample (`a ≥ 0`). Add `true_or, or_true, not_or` to the simp set. Wrap it in a `local macro "fin_omega"` with a second `first` branch that simps `at *` when the needed facts are hypotheses (e.g. `hj : j.val = n`).