mathport ∀ a b c ∈ s

Stream: mathlib4

[Winston Yin]

I've noticed that mathport expands the syntactic sugar ∀ a b c ∈ s differently than Lean3. The Lean3 ordering is

∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → ∀ (c : α), c ∈ s → ...

while mathport gives

∀ (a b c) (_ : a ∈ s) (_ : b ∈ s) (_ : c ∈ s)

This actually causes some golfed proofs to fail

[Winston Yin]

Should I submit an issue?

[Mario Carneiro]

update lean?

[Mario Carneiro]

lean 3 was modified specifically because of this issue

[Winston Yin]

You mean update Lean4?

[Mario Carneiro]

hm, no I mean lean 3

[Mario Carneiro]

but it seems that even though lean#656 was intended to simplify mathport, the corresponding mathport change was never done once it landed

[Yaël Dillies]

Whar order are we settling on in mathlib 4? ∀ (a : α), a ∈ s → ... has the advantage that it can be handled as a block, and it directly relates to decidability instances for finset.

[Mario Carneiro]

We moved to the ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → ∀ (c : α), c ∈ s → ... order a while ago

[Mario Carneiro]

pretty sure that's what the mathlib4 binder syntax expands to as well

[Mario Carneiro]

but the "expanding binder collection" warning is because we don't actually want to be expanding these binders, we should use the same binder syntax that lean 3 is using. Mathport hasn't been updated for the mathlib4 implementation of binder collections I think

[Patrick Massot]

We probably need someone to hunt down those comments in mathlib4

[Mario Carneiro]

probably better to look for them in mathlib3port, since people are likely deleting them in mathlib4