forall_swap etc for a `Type*` and a `Prop`

Stream: mathlib4

[Yury G. Kudryashov]

What do you think about making docs#forall_swap a simp in a special case α : Type* β : Prop? Same about iSup, iUnion, iInf etc.

[Yury G. Kudryashov]

See, e.g., this comment by @Yaël Dillies for motivation.

[Yaël Dillies]

So move all the types inward and all the props outward? Interesting...

[Yury G. Kudryashov]

Currently, docs#exists_and_left is a @[simp] lemma. IMHO, forall_imp_swap {α : Type*} {p : Prop} {q : α → p → Prop} := @forall_swap α p q is very similar.

[Kyle Miller]

This might be a good use for simprocs, where a simproc could do the transformation all at once rather than doing it as a bubble sort. I don't have any intuition though whether the transformation is a good idea or not in general.

[Eric Wieser]

I would guess that the number of binders is rarely above 6, so a bubble sort isn't really all that bad

[Eric Wieser]

Which is to say: let's try the lemma version and benchmark before expending effort on the simp proc

[Mario Carneiro]

I would be concerned about performance, I'm not sure how good the indexing is wrt universes