feat: prop instance yields theorems

[kmill]

This PR adds a feature to the the mutual def elaborator where the instance command yields theorems instead of definitions when the class is a Prop.

Closes #5672

[kmill]

@Kha The way I got this to work was by adding an extra DefKind for instances that's basically the same as for defs, but when the declaration is finally added to the environment, it checks to see if the type is a Prop to decide whether to use a theorem or a definition.

Instances then follow def variable inclusion rules instead of theorem. I had thought about modifying header processing to see whether the type is a prop and change the kind to def or theorem at that moment, to get theorem inclusion rules, but then if you omit the type it would use def inclusion rules. That seems confusing.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5856 build failed against this PR. (2024-10-27 00:24:02) View Log
• ✅ Mathlib branch lean-pr-testing-5856 has successfully built against this PR. (2024-10-27 02:38:46) View Log