feat: allSome_length

[Smaug123]

• I'm not very fluent with Lean, and there may certainly be better ways to prove this. In particular, I'm using a lot of simp to reduce the unfold.
• Is your intuition that this will become more ergonomic to use if e.g. the res parameter were made implicit?
• Should this be simp?

[Smaug123]

awaiting-review

[fgdorais]

These theorems should be in Batteries.Data.List.Lemmas. (Batteries.Data.List.Basic is about definitions, and the occasional lemma that is needed for a later definition.)

[Smaug123]

I'm not convinced this theorem is architecturally the right choice; it seems very special-casey. Something more "if isSome then all the elements are the same", from which this could be deduced, seems more reasonable to me.