Lean/Mathlib: which tactics fail on 'no progress' (and Lean 4 has no tactic <|>)

Tested on Mathlib v4.35.0 and v4.36.0-rc2. Goals were x < y (x y : ℕ), a < b and a = b (a b : ℚ), with no hypotheses, each run as fail_if_success T on its own line.

These succeed silently and leave the goal unchanged: norm_num, norm_num1, push_cast, norm_cast.

These fail: simp, simp only [], simp?, simp_arith, ring_nf, ring, abel, abel_nf, field_simp, omega, linarith, nlinarith, positivity, gcongr, linear_combination.

Consequence: inside first | A | B, a silent-success tactic commits to its branch. Write first | (norm_num; done) | exact h, which falls back correctly. ring fails here only because its ring_nf fallback also fails (the macro is first | ring1 | try_this ring_nf). When ring_nf can rewrite something without closing the goal, ring succeeds and leaves the goal open. Use ring1 inside first.

Side observation: with h : x < y in context, norm_cast alone closed x < y, while norm_num and push_cast did not.

Syntax gotcha: Lean 4 has no tactic-level <|>. skip <|> exact h gives unexpected token '<|>'; expected command, in plain Lean (v4.9.0, v4.20.0, v4.35.0, v4.36.0-rc2) and with Mathlib imported. Only first | A | B exists. The <|> in Init/Notation.lean is for terms (HOrElse) and syntax categories.

Testing tip: put fail_if_success T on its own line. fail_if_success T; sorry on one line takes T; sorry as its argument.