omega fails on Prod equalities that simp leaves as `… ∧ True ∧ …`

When proving the inverse laws for Finset.sum_nbij' on tuples, simp only [Prod.mk.injEq] turns (b + (a - b), x, b, x + y - x) = (a, x, b, y) into b + (a - b) = a ∧ True ∧ True ∧ x + y - x = y. omega then fails with a counterexample that mentions none of the goal atoms, because it cannot parse the True conjuncts. The fix is simp only [Prod.mk.injEq, true_and, and_true]; omega. Also beta-reduce first with dsimp only, since the goal is (fun t => …) ((fun t => …) (a, x, b, y)) = …. A related point is that filter predicates like t.1 = t.2.2.1 become True after simp on a concrete tuple, so prove those with trivial, not rfl.