fix: missing propagation in grind (#6528)

This PR adds a missing propagation rule to the (WIP) `grind` tactic.

src/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -99,6 +99,8 @@ builtin_grind_propagator propagateNotUp ↑Not := fun e => do
   else if (← isEqTrue a) then
     -- a = True → (Not a) = False
     pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
+  else if (← isEqv e a) then
+    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
 /--
 Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`.

tests/lean/run/grind_propagate_connectives.lean

@@ -103,3 +103,6 @@ example (p q r : Prop) : p ∨ (q ↔ r) → ¬r → q → False := by
   grind on_failure do
     Lean.logInfo "hello world"
     fallback
+
+example (a b : Nat) : (a = b) = (b = a) := by
+  grind