fix: assertion violations at grind checkInvariants (#9700)

This PR fixes assertion violations when `checkInvariants` is enabled in
`grind`

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

@@ -384,6 +384,7 @@ where
           -- We must swap the congruence root to ensure `isDiseq` and `getDiseqFor?` work properly
           modify fun s => { s with congrTable := s.congrTable.insert { e := n.self } }
           setENode n.self { n with congr := n.self }
+          setENode e { (← getENode e) with congr := n.self }
 
 /-- Ensures collection of equations to be processed is empty. -/
 private def resetNewFacts : GoalM Unit :=

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

@@ -47,8 +47,8 @@ def addCongrTable (e : Expr) : GoalM Unit := do
       we must ensure that `e` is still the congruence root.
       -/
       modify fun s => { s with congrTable := s.congrTable.insert { e } }
-      let node ← getENode e'
-      setENode e' { node with congr := e }
+      setENode e' { (← getENode e') with congr := e }
+      setENode e { (← getENode e) with congr := e }
     else
       let node ← getENode e
       setENode e { node with congr := e' }