Missaligned type between Lean 3 and Lean 4 with ∃

Stream: mathlib4

[Arien Malec]

I remember reading a Zulip thread about this, but can't find it...

In Lean 4, the following:

theorem signBijAux_surj {n : ℕ} {f : Perm (Fin n)} :
    ∀ a ∈ finPairsLT n, ∃ b ∈ finPairsLT n, a = signBijAux f b

is being typed as {n : ℕ} {f : Perm (Fin n)} (a : (_ : Fin n) × Fin n) (a✝ : a ∈ finPairsLT n) : ∃ b, b ∈ finPairsLT n ∧ a = signBijAux f b with an ∧ but previously was typed as:

{n : ℕ} {f : perm (fin n)} (a : Σ (a : fin n), fin n), a ∈ fin_pairs_lt n → (∃ (b : Σ (a : fin n), fin n) (H : b ∈ fin_pairs_lt n), a = f.sign_bij_aux b)

[Arien Malec]

I assume there's a simple fix here to make the desired types align....

[Eric Wieser]

Writing ∃ twice might achieve the lean 3 behavior

[Eric Wieser]

Though I think maybe the port is intended to make us switch to the new spelling?

[Arien Malec]

Maybe, but there's an upstream dependency on the signature. I fixed this by typing the exact equivalent of the Lean 3 type:

theorem signBijAux_surj {n : ℕ} {f : Perm (Fin n)} :
    ∀ a ∈ finPairsLT n, ∃ (b: Σ (_: Fin n), Fin n) (_H: b ∈ finPairsLT n), a = signBijAux f b

[Yury G. Kudryashov]

I usually change ∃ i, ∃ h : p i, _ to ∃ i, p i ∧ _ while porting.

[Yaël Dillies]

This sounds quite breaking, Yury. Some proofs shuffle the ∃ around.

[Yury G. Kudryashov]

Quite often we do this change without noticing because ∃ x ∈ s, p x changed its meaning.

[Yaël Dillies]

I know, and I think we should work against it, although this will of course look much uglier :frown:

[Johan Commelin]

@Yaël Dillies It doesn't really seem to be a problem in practice.

[Yury G. Kudryashov]

If we work against it now, then we'll have to revert it back to ∃ x ∈ s, p x later. I think that it's less work if we do it now.