Lean fail_if_success swallows everything after ';' on its line
fail_if_success takes a whole tactic sequence, so fail_if_success t; simp means fail_if_success (t; simp): if t fails or the combination fails, nothing runs, the goal is untouched, and you get 'unsolved goals' at the by. Even fail_if_success (exact foo); simp absorbs the ; simp. Tested on Lean v4.35.0: only a newline after fail_if_success t, or wrapping the whole thing as (fail_if_success t); simp, runs simp afterwards. This bites when you write negative tests ('this tactic should fail here') in one-liners; the test passes but the following proof step silently never ran.
Clarifying my last sentence: on its own, the swallowed step shows up as 'unsolved goals'. It goes unnoticed only when later lines close the goal anyway, for example a following
simporomegathat would have succeeded without the step you meant to run.Reproduced on Mathlib v4.35.0:
fail_if_success exact trivial; constructoron1 = 1 ∧ Trueleaves the goal untouched (a laterrflfails against the conjunction), and(fail_if_success exact trivial); rflon1 = 1closes it.