Locations for list lemmas?

Stream: mathlib4

[David J. Webb]

In the course of my current computability PR, I ended up needing to state a handful of lemmas purely about lists - so they should really be placed somewhere besides Computability:

lemma filter_length_ne_zero_iff : ((fun L ↦ filter (fun a ↦ f a b) L) L).length ≠ 0 ↔ (∃ a ∈ L, f a b)

lemma filter_length_eq_length_iff : ((filter (f · b) L)).length = L.length ↔ (∀ a ∈ L, f a b)

lemma filter_eq_filtermap_ite : L.filter (fun a ↦ f a b) = filterMap (fun a ↦ if f a b then some a else none) L

I was planning to put them all in Data.List.Basic, but I figured I'd ask if anyone had any better ideas. #find_home only suggests that location for the last lemma, whereas it suggests Batteries.Data.List.Basic for the other two, which doesn't feel right to me.

(I'm also not completely sold on the name of the last one - open to suggestions!)

[Kim Morrison]

These are stated very strangely! The first should be (L.filter f).length ≠ 0 ↔ ..., etc.

I don't understand the purpose of the b in any of the statements above.

[Kim Morrison]

Lemmas about List can go in Data.List.Basic, although if they are genuinely missing lemmas about basic operations, you probably should tell me about them and I'll put them in the core library.

[David J. Webb]

Originally they were all have statements inside of the actual theorems, but grunweg asked me to extract them since they're purely about lists.

I'm just as happy to tuck them back into their respective theorems - only the third one is actually used more than once (and only twice, at that).

[David J. Webb]

Also @Yaël Dillies caught the weird phrasing, it looks like, I just hadn't seen those suggestions yet!

[David J. Webb]

Thankfully I was able to simplify these down and eliminate two all of them from the PR, which cleans things up substantially