exact? test failure: le_antisymm vs ge_antisymm

Stream: mathlib4

[Ruben Van de Velde]

test/LibrarySearch/basic.lean:228:2: error: Tactic `exact?` produced `exact ge_antisymm hyx hxy`,
but was expecting it to produce `exact le_antisymm hxy hyx`!

Seems unfortunate to fail CI over that

[Eric Wieser]

Arguably that's a bug in exact?; it should be preferring docs#le_antisymm over docs#ge_antisymm

[Jireh Loreaux]

why do we even have docs#ge_antisymm ?

[Ruben Van de Velde]

Good question, I assumed it would be in core, but it's in mathlib

[Notification Bot]

4 messages were moved here from #mathlib4 > Obscure test fail by Eric Wieser.

[Yaël Dillies]

ge_antisymm was an ematch lemma in Lean 3. The port should have deleted it in favor of le_antisymm.

[Ruben Van de Velde]

Thanks for volunteering to remove it :)

[Yaël Dillies]

#8760

[Yaël Dillies]

I see you were talking about ge_antisymm, not le_antisymm'. I added ge_antisymm ages ago to make sure the API is symmetric (sometimes one ≤ is much eaier than the other, and you want it to come last).

[Yaël Dillies]

This is also useful for dualising proofs without having to shuffle arguments.

[Ruben Van de Velde]

Yeah, not sure what made you think about le_antisymm'

[Yaël Dillies]

Well, it's an exact copy of le_antisymm, so that was fitting with exact? getting confused.

[Yaël Dillies]

Seems I was quite spot on :smile: : https://github.com/leanprover-community/mathlib4/actions/runs/7057097484/job/19210170676

[Winston Yin (尹維晨)]

Getting the same CI error in #8397. Is there a fix?

[Eric Wieser]

I think the fix was merged yesterday; have you merged master recently?

[Winston Yin (尹維晨)]

Merged master again just now. Problem went away. Thanks!