refactor(tactic/ring): split off `ring_nf` tactic (#6792)
[As requested on Zulip.](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ring.20not.20idempotent/near/231178246) This splits the current behavior of `ring` into two tactics:
* `ring1`: closing tactic which solves equations in the goal only
* `ring_nf mode? (at h)?`: simplification tactic which puts ring expressions into normal form
The `ring` tactic will still call `ring1` with `ring_nf` as fallback, as it does currently, but in the latter case it will print a message telling the user to use `ring_nf` instead. The form `ring at h` is removed, because this never uses `ring1` so you should just call `ring_nf` directly.
