feat: instances should always be non-recursive

[Kha]

This PR changes the instance commands to no longer be accepted in mutual blocks and not to accept recursive uses of the instance name, if any. Such uses were problematic in two ways: first, one could assume that by being able to place instance in mutual, the instances would be able to refer to each either implicitly but this has never been the case; instance used to behave like def in there and so it is better to be explicit about that by writing separate defs. Second, instances have special reducibility, @[instance_reducible] by default. The implementation of an instance, where the recursive use happens, should not have this reducibility, so even for non-structure classes, a separate implementation recursive def (or where) should be used.

Breaking changes

instance commands to no longer are accepted in mutual blocks and do not accept recursive uses of the instance name, if any.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-04 12:59:43)