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)

Author: JovanGerb

Mathlib/Order/Antisymmetrization.lean

@@ -84,6 +84,23 @@ theorem antisymmRel_iff_eq [IsRefl α r] [IsAntisymm α r] : AntisymmRel r a b 
 
 alias ⟨AntisymmRel.eq, _⟩ := antisymmRel_iff_eq
 
+namespace Mathlib.Tactic.GCongr
+
+variable {α : Type*} {a b : α} {r : α → α → Prop}
+
+lemma AntisymmRel.left (h : AntisymmRel r a b) : r a b := h.1
+lemma AntisymmRel.right (h : AntisymmRel r a b) : r b a := h.2
+
+/-- See if the term is `AntisymmRel r a b` and the goal is `r a b`. -/
+@[gcongr_forward] def exactAntisymmRelLeft : ForwardExt where
+  eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``AntisymmRel.left #[h])
+
+/-- See if the term is `AntisymmRel r a b` and the goal is `r b a`. -/
+@[gcongr_forward] def exactAntisymmRelRight : ForwardExt where
+  eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``AntisymmRel.right #[h])
+
+end Mathlib.Tactic.GCongr
+
 end Relation
 
 section LE

MathlibTest/GRewrite.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Zimmer, Mario Carneiro, Heather Macbeth, Jovan Gerbscheid
 -/
 import Mathlib.Data.Int.ModEq
+import Mathlib.Order.Antisymmetrization
 import Mathlib.Tactic.GRewrite
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.NormNum
@@ -320,3 +321,22 @@ example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
 example (h₁ : a ∣ b) (h₂ : b ∣ a * d) : a ∣ b * d := by
   grw [h₁] at h₂ ⊢
   exact h₂
+
+namespace AntiSymmRelTest
+
+variable {α : Type u} [Preorder α] {a b : α}
+
+local infix:50 " ≈ " => AntisymmRel (· ≤ ·)
+
+axiom f : α → α
+
+@[gcongr]
+axiom f_congr' : a ≤ b → f a ≤ f b
+
+example (h : a ≈ b) : f a ≤ f b := by
+  grw [h]
+
+example (h : b ≈ a) : f a ≤ f b := by
+  grw [h]
+
+end AntiSymmRelTest