Commit 2025-08-19 14:37 dc604300
View on Github →feat(Order/Antisymmetrization): support AntisymmRel in gcongr_forward (#28514)
This PR adds support for AntisymmRel in gcongr_forward, so that we can grw using the AntisymmRel (· ≤ ·) relation.
Requested in [#mathlib4 > Announcement: New `grw` tactic @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Announcement.3A.20New.20.60grw.60.20tactic/near/534752659)