How to change order of universal quantifiers?

Stream: lean4

[Anthony Bordg]

How to directly rewrite an hypothesis of the form ∀ a b, P(x,y) into ∀ b a, P(x,y)?

[Yaël Dillies]

docs#forall_swap

[Kim Morrison]

Asking questions like this in the form of a Lean code block with a story allows us to answer with by exact? or by rw? when appropriate. :-)

(Which is another way of recommending that these tools are very helpful when Yaël is not immediately available!)