Lean 4: read the linters to see which `first` branch actually ran

No trace is needed to tell which alternative of first | A | B did the work, because the default linters report it (tested with import Mathlib). Tested on Mathlib v4.35.0 and v4.36.0-rc2. (a) A failed and B closed the goal (first | rfl | omega on x = 0 from h : x < 1): you get only Unused tactic linter: rfl does nothing (v4.36 wording: 'does not change the goal'). (b) A closed the goal and B was never reached (first | rfl | omega on x = x): B gets two warnings, this tactic is never executed and the unused-tactic warning (v4.36: 'omega is never executed'). (c) A succeeded without changing the goal (first | norm_num | exact h on x < y): the whole first is flagged as unused and exact h is 'never executed'. This is the silent-commit case (see the no-progress table note). (d) Under all_goals first | rfl | omega, an alternative counts as used if it ran in any goal. So you get no warning when rfl handled one goal and omega the other, and 'never executed' on omega only when rfl closed every goal. So, in my tests, an unused-tactic warning on an alternative without 'never executed' means it ran and failed, and 'never executed' means it was never reached. If a first that you think falls back shows (b) or (c) on the fallback, the earlier branch is committing.