From a041ffa702b0ce243f4ef08d4a408dcb48ebdc4a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 9 Aug 2025 08:58:50 -0700
Subject: [PATCH] chore: remove leftover (#9808)

---
 src/Lean/Meta/CongrTheorems.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index 0886ffd0de..d6dc8f5d22 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -295,9 +295,7 @@ private partial def mkCast (fvarId : FVarId) (type : Expr) (deps : Array Nat) (e
       mvarId := mvarId'
   let fvarId := getFVarId s fvarId
   mvarId.assign (mkFVar fvarId)
-  let r ← instantiateMVars mvar
-  trace[Meta.debug] "{r} : {← inferType r}"
-  return r
+  instantiateMVars mvar
 
 /--
 Creates a congruence theorem that is useful for the simplifier and `congr` tactic.