From dba358067ae20ea8a940ab67ffe4c176f22f478b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Sep 2021 22:37:20 -0700
Subject: [PATCH] chore: remove workaround

---
 src/Lean/Meta/Tactic/Contradiction.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean
index 9121ee90b6..2ae0002013 100644
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@@ -55,7 +55,7 @@ partial def elim (mvarId : MVarId) (fvarId : FVarId) : M Bool := do
               if (← elim subgoal.mvarId field.fvarId!) then
                 return true
         return false
-      unless found == true do -- TODO: check why we need true here
+      unless found do
         return false
     return true