feat: Port the map part of bi/big_op.v

[lzy0505]

Description

Part of #113.

Ported big_[and/sep]M.

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

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[markusdemedeiros]

A couple changes but overall this looks great

[markusdemedeiros]

This is the only proof I'd insist be cleaned up before merging, it's very hard to read. Big .trans terms can be changed to calc blocks or refines, non-terminal simps should be squeezed or eliminated. Happy to give it a look myself!

[lzy0505]

Thanks for reviewing! I've addressed all comments but the last one on bigSepM_impl_strong. Please give it a look.

[markusdemedeiros]

Merged! bigSepM_impl_strong is indeed pretty hard to clean up. I didn't want to let it block the project any longer so I just broke up those big terms into refine sequences and added a FIXME for later.