feat: implement imodintro and imod

[MackieLoeffel]

Description

This PR implements the imodintro tactic and adds the !> intro pattern for introducing modalities.
Additionally, it implements imod and the > cases pattern.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

@lzy0505 This PR is ready to review.

[lzy0505]

Great PR! I’ve added some code comments. A minor improvement would be the error message for inext. You can see it in the last test case I added. The PR is ready to merge anyway.

[MackieLoeffel]

Thanks for the review and the changes! It is a bit tricky to tweak the error for inext, so I would leave it as is for the moment.