Quotient.eq

Stream: general

[Violeta Hernández]

I'm trying to update my Rubik's cube project to Lean v.4.13 and I'm running into an issue with Quotient.eq. Specifically, the rewrite rw [← Quotient.eq] at x ≈ y no longer yields ⟦x⟧ = ⟦y⟧.

[Violeta Hernández]

I imagine this is due to one of @Yuyang Zhao's recent refactors, but I'm not quite sure what the intended fix is. Am I just supposed to not use ≈ notation for quotients?

[Violeta Hernández]

Or is the idea that every quotient type declares its own Quotient.eq lemma using the preferred form of the setoid relation?

[Violeta Hernández]

For the moment I fixed my code by simply making .eq lemmas for the quotients I was working with

[Yuyang Zhao]

This is #17594. Currently you can use docs#Quotient.eq_iff_equiv.