bump - missing automation?

Stream: general

[Eric Rodriguez]

on branch#ericrbg/lean_bump, I'm trying to bump to 3.36.0 (and I guess soon 3.36.1). the main breaking change in this is that the binders ∀ x y ∈ s are now ∀ x, x ∈ s → ∀ y, y ∈ s instead of ∀ x y, x ∈ s → y ∈ s. this should not add anything more than tedium but can be quite annoying to deal with, see for example:

https://github.com/leanprover-community/mathlib/blob/0693aeb996512dc8aabd0130b53c87e7f70fb9ab/src/topology/uniform_space/basic.lean#L947

and it gets a bit more annoying in /src/topology/uniform_space/cauchy.lean (I haven't fixed this file yet because of this). my question is, am I missing some tactics/lemmas for this? tauto, finish, simp don't seem to help too much. or is the right approach to refactor lemmas that are of the form ∀ x y, p x → p y to the new binder form? although that breaks plenty of other things, too, so I'm not too sure that's optimal either.

[Mario Carneiro]

could you explain the tedium in that example a bit more? It's hard to tell what the issue is without building it

[Yaël Dillies]

It seems like this new binder form is generally preferable because you give away the information more granularly. I am myself guilty of using ∀ x y, x ∈ s → y ∈ s in some convexity stuff, and docs#convex still uses them.

[Eric Rodriguez]

well the example I linked is now a whole begin...end, but it used to be a simp with two arguments

[Mario Carneiro]

right, what caused the simp to break?

[Reid Barton]

apparently a change in Lean:

the main breaking change in this is that the binders ∀ x y ∈ s are now ∀ x, x ∈ s → ∀ y, y ∈ s instead of ∀ x y, x ∈ s → y ∈ s

[Reid Barton]

and presumably the old order conveniently lined up with some other definition in a way that the new one doesn't

[Eric Rodriguez]

image.png

this is the goal state after simp_rw prod.forall; before this would've been in the "right" order automatically but now there neds to be reordering

[Mario Carneiro]

yes I'm aware of that (I wrote that change), but I'm wondering what definitions are specifically encouraging the old order

[Mario Carneiro]

You might have some luck with an (unannotated) simp lemma saying (∀ x y, x ∈ s → y ∈ t → p) <-> (∀ x, x ∈ s → ∀ y, y ∈ t → p)