fix(tactic/rcases): fix rcases? goal alignment (#5576)
This fixes a bug in which `rcases?` will not align the goals correctly
in the same manner as `rcases`, leading to a situation where the hint
produced by `rcases?` does not work in `rcases`.
Also fixes a bug where missing names will be printed as `[anonymous]`
instead of `_`.
Fixes #2794
