instance assuming AC

Stream: general

[FR]

I noticed that the instance src#left_cancel_semigroup.contravariant_mul_le_of_contravariant_mul_lt uses the lemma src#le_iff_eq_or_lt, which needs to assume AC. This leads to some lemmas also assuming AC even for natural numbers.
Is there any good way to make it do not need to assume AC for the types with docs#decidable_eq?

[Yaël Dillies]

Are you doing this for yourself or for mathlib? mathlib is resolutely classical so we couldn't care less.

[FR]

But mathlib still preserves some lemmas that explicitly attempt to avoid AC in decidable namespace? I suspected that someone might care about it.

[Yaël Dillies]

There are 45 such lemmas across all of mathlib, 83760 lemmas in total (although maybe half are autogenerated).