feat: proofs for Batteries.Data.Array/Vector.Monadic

[Rob23oba]

Adds proofs for the proof_wanteds in Batteries.Data.Array.Monadic.

[kim-em]

@Rob23oba, thank you, these are very nice!

[kim-em]

I'll wait until Monday to merge this, so your commit ends up directly on main, rather than bundled into the v4.17.0 update. I presume/hope that you're happy if I move this material up to Lean itself quite soon?

[Rob23oba]

Sure, very cool!

[fgdorais]

Excellent work! There's a lot of nonterminal simps. Could you go through and squeeze them using simp??

[Rob23oba]

There you go, replaced all of my simps I could find.

[Rob23oba]

I've added LawfulFunctor.map_inj_right_of_nonempty and LawfulMonad.map_inj_right because they are very useful in proving the other statements. However, they are definitely in the wrong place and from what I've seen it is also very uncommon to put lemmas about a class into the namespace of the class. So, anyone know where a better place to put these would be?

[Rob23oba]

Oh, I didn't realize you already made LawfulFunctor.map_inj_right_of_nonempty as map_inj_of_inj in core lean! The one there doesn't need Applicative though, Functor is enough. But we also definitely need the one with LawfulMonad because that's the more common case and that one doesn't require Nonempty. We might want to change the naming a bit then (e.g. map_inj_of_inj for the monadic one, map_inj_of_inj_of_nonempty for the functor one) to make sure we have both.