feat: clarify warning for semireducible definitions of class type

[datokrat]

This PR improves on the warnings and errors regarding reducibility attributes. Partially addresses #13351.

• When trying to add a semireducible attribute, do not claim it is the default; it is not in the case of instance declarations.
• Allow users to disable the reducibility warning on instances.
• Do not warn on @[irreducible] instance declarations, in analogy to how we do not warn on attribute [instance] irreducibleDecl.

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-06-26 13:37:40) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-06-26 13:39:01) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-06-26 14:07:40) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-06-26 14:09:15) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-08 07:55:50) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-08 07:56:49) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-09 13:55:53) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-09 13:57:04) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 08:43:06) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-10 08:44:15) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 09:54:47) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-10 09:56:19) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 11:25:17) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-10 11:26:27) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 11:58:29) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-10 11:59:50) View Log
• ✅ Reference manual branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 13:09:09) View Log
• 🟡 Reference manual branch lean-pr-testing-14196 build against this PR didn't complete normally. (2026-07-10 13:10:20) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14196 has successfully built against this PR. (2026-06-26 15:04:14) View Log
• 💥 Mathlib branch lean-pr-testing-14196 build failed against this PR. (2026-07-08 08:42:05) View Log
• ✅ Mathlib branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-09 15:03:50) View Log
• ✅ Mathlib branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 09:42:08) View Log
• ✅ Mathlib branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 10:52:36) View Log
• ✅ Mathlib branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 12:55:12) View Log
• ✅ Mathlib branch lean-pr-testing-14196 has successfully built against this PR. (2026-07-10 14:11:08) View Log