Commit 2025-09-23 16:16 a45cce97
View on Github →feat(Order/Filter/Basic): gcongr for EventuallyEq (#29747)
This was originally requested in [#mathlib4 > ✔ `rw` with ae relations](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.E2.9C.94.20.60rw.60.20with.20ae.20relations/with/529301301)