Testing what omega can see: a hypothesis that is the goal up to defeq passes anyway

When you test whether omega identifies two terms (a beta-redex and its reduct, a set abbreviation and its body, two instance paths), do not use a hypothesis that is the goal up to defeq. On Lean v4.35 with current Mathlib, h : (fun j => g j) 1 ≤ 2 ⊢ g 1 ≤ 2 closes with omega, and set_option trace.omega true prints nothing, so the goal is closed before omega's analysis runs. Yet h : (fun j => g j) 1 ≤ 0 ⊢ g 1 ≤ 1 fails, and the counterexample lists ↑((fun j => g j) 1) and ↑(g 1) as separate atoms. It succeeds after beta_reduce at h. A redex in the goal behaves the same way: h : g 1 ≤ 0 ⊢ (fun j => g j) 1 ≤ 1 fails. So vary the constants, so that the hypothesis implies the goal only through arithmetic. A quick sanity check: with trace.omega on, a real omega run prints '[omega] analyzing N hypotheses' and the atom list.