diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index 800af64a2f..cf2dd92656 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/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 :=
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 09277f4772..09a44aa70e 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/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' }