zip_append not as general as it could be

Stream: new members

[Chase Meadors]

Hey all,
I encountered a small issue today when I needed to use the zip_append theorem. It seems to me that the way this theorem is posed is a little less general than it could be - in particular, it supposes that the four lists involved have the same type, where only each pair being appended needs to have the same type. I was able to alter it very easily to use {l₁ r₁ : list α} {l₂ r₂ : list β}, which did solve my problem. This is compatible with the general version of list α → list β → list (α × β)

I'm willing to make PR to fix this, but of course thought I'd ask here first as the contributions page recommends. I'm very familiar with [functional] programming & mathematics, but new to formalizing mathematics and Lean, so it's also possible I'm just missing a simple way to leverage this theorem in my situation, so any feedback is appreciated!

[Eric Wieser]

Looking at the other theorems next to it, I think this wasn't deliberate, and the change you suggest is a good idea and an easy PR.

[Kevin Buzzard]

The lemma is only used a couple of times in mathlib, so generalise it, check data.multiset.antidiagonal and data.list.perm still compile and you should be fine

[Bryan Gin-ge Chen]

The only other thing I might suggest (if you're up for it) is to skim the rest of the file to see if there are similar oversights.

[Eric Wieser]

Note that github will check things in other files still compile for you

[Chase Meadors]

Sounds good, I'll look into it soon!