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