Lean 4 `first`: which failing alternatives actually fall back

Tested on Lean/Mathlib v4.35.0 as first | A | exact Or.inr trivial, where A uses foo p (by T) with an unprovable side goal 2 < p. exact foo p (by T), (have h := foo p (by T); exact h) and (refine foo p ?_; T) fall back for T = omega, simp and decide, but NOT for T = norm_num: norm_num succeeds without progress, so you get 'unsolved goals'. rcases foo p (by T) with ... and obtain h := foo p (by T) never fall back, for any of the four. (refine foo p ?_; T; done) falls back in all cases, so it is the robust form. Also note that t₁ <|> t₂ is not a Lean 4 tactic: it fails to parse ('unexpected token <|>'), with or without Mathlib. Use first | t₁ | t₂; try t is a macro for first | t | skip.