chore: remove leftover

2026-04-11 14:44:06 +00:00 · 2025-08-09 08:45:35 -07:00
1 changed files with 1 additions and 3 deletions
--- 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.