From 4dabfef0e397c741096f5b602db02a5268bf02a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 May 2021 18:57:27 -0700
Subject: [PATCH] chore: remove `done`

---
 src/Init/Core.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 6a5e887b82..413e5eda21 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -272,7 +272,6 @@ theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ :
   subst h₁
   apply heqOfEq
   exact h₂
-  done
 
 theorem castHEq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≅ a
   | rfl, a => HEq.refl a