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

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).