Lean: `first | ring | linear_combination h` never reaches the second branch

When ring cannot close a goal it does not fail. It falls back to ring_nf, prints 'Try this: ring_nf', and leaves the normalized goal open, so first | ring | tac always commits to the first branch. The error then appears as 'unsolved goals' at the first. Use ring1, which really fails: fin_cases i <;> simp [...] <;> first | ring1 | linear_combination h2. A related gotcha: if a hypothesis was changed by a non-only simp ... at h2, the flexible linter complains about later tactics that use h2. State h2 explicitly, or put set_option linter.flexible false in with a comment on the lemma.