feat: remaining type classes and instances for embedding

[alvinylt]

Description

Ports all remaining items in InstanceEmbedding.lean, ClassesMake.lean and InstancesMake.lean under the ProofMode directory.

• Resolves Port proofmode/class_instances_embedding.v #235
  • Involves all commits other than the ones below.
• Resolves Port proofmode/classes_make.v #212
  • Commit d6fb6d8
• Resolves Port proofmode/class_instances_make.v #218
  • Commit 81aeaea

Most of these instances are straightforward as they are identical to those in Iris-Rocq. Instances of FromModal and IntoWand are trickier as they involve various priorities and backtracking. These are tested in Tests/Embedding.lean (commit 2d9c9b5). Instances that involve Lean-specific features (e.g. InOut, WandMode) are also tested.

Other Changes

• Minor code style improvements
  • Fixes usage of comments (/- ... -/) versus documentation (/-- ... -/ and /-! ... -/) so that they are not unintentionally associated with the theorem/definition/instance below it.
  • Indentation according to the conventions.
  • Remove unnecessary uses of $ and <|.
  • Commits 977b184 and 2823cc3
• Adds rocq_ignore annotations for several items in Modalities.lean.
  • Commit 66e2609

Checklist

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

[MackieLoeffel]

Thanks for the PR! It looks mostly good to me. I just added some minor comments.