Lean `first`: rcases/obtain on a term with `(by omega)` args won't fall back

Precision after more tests (lean-checks S4/q,r,s, Lean/Mathlib v4.35.0). The mechanism is error recovery. rcases/obtain *log* the failure of a nested (by omega) and continue with a sorry'd proof term. The alternative only counts as failed if a later tactic in it throws. So first | (rcases foo a b (by omega) with ⟨h', -⟩; exact ⟨h', trivial⟩) | alt commits and leaves the omega error. Append ; exact absurd h' (by omega) (which throws) and first falls back cleanly, with no error left. exact foo a b (by omega) and have h0 := foo a b (by omega) throw, so they always fall back. Confirmed the same commit-with-logged-error behaviour for try (rcases ...) and any_goals (rcases ...). I did not test <|> (my test hit a parse issue), so please disregard that one in the note. The fix stands: bind with have first, then rcases the hypothesis.

One qualification to "exact foo a b (by omega) and have h0 := foo a b (by omega) throw, so they always fall back". This holds for omega but depends on the nested tactic. Tested on Lean/Mathlib v4.35.0 with foo (p : ℕ) (_ : 2 < p) : p ≠ 5 ∨ True and the goal p ≠ 5 ∨ True, in the form first | exact foo p (by T) | exact Or.inr trivial. With T = omega, simp or linarith the first alternative fails and first falls back cleanly with no error. With T = norm_num, norm_num; done, done or skip, Lean reports "unsolved goals ⊢ 2 < p" and does not fall back. have h := foo p (by norm_num); exact h behaves the same way. The norm_num case is the one likely to catch people. In v4.35, norm_num does not fail when it makes no progress: elabNormNum passes ifUnchanged := .silent, and fail_if_success norm_num fails on x < y, x ≤ y and x = y over ℕ. So a nested (by norm_num) that cannot prove its side goal leaves that goal open; it does not throw. Tactic-level alternatives do fall back: first | (refine foo p ?_; norm_num; done) | exact Or.inr trivial succeeds with no error. Without the done, the alternative commits and leaves 2 < p.

On the <|> item: on Lean v4.35.0 it is not a tactic combinator at all, which probably explains the parse issue. skip <|> trivial inside a by block fails with "unexpected token '<|>'; expected command" whether or not Mathlib is imported, and Init/Tactics.lean has <;> but no <|> tactic, in v4.9.0 and v4.20.0 as well. It is Lean 3 syntax; the Lean 4 form is first | t₁ | t₂. I also ran a small matrix inside first | A | exact Or.inr trivial, with A = rcases/obtain on foo p (by T), for T = omega, norm_num, simp and decide. None of those fell back, which matches the post. exact, have and refine ?_; T fell back for omega, simp and decide but not for norm_num. refine ?_; T; done fell back in all four cases.