diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index bfcf686861..93bef111cf 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -317,7 +317,7 @@ where
     let args := e.getAppArgs
     for arg in args, kind in cgrThm.argKinds do
       match kind with
-      | CongrArgKind.fixed => argsNew := argsNew.push arg
+      | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg)
       | CongrArgKind.cast  => hasCast := true; argsNew := argsNew.push arg
       | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg
       | CongrArgKind.eq =>