diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 4a1b70c88e..dc352f154f 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -606,8 +606,8 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α}
 theorem PUnit.subsingleton (a b : PUnit) : a = b := by
   cases a; cases b; exact rfl
 
-@[simp] theorem PUnit.eq_punit (a : PUnit) : a = () :=
-  PUnit.subsingleton a ()
+@[simp] theorem PUnit.eq_punit (a : PUnit) : a = ⟨⟩ :=
+  PUnit.subsingleton a ⟨⟩
 
 instance : Subsingleton PUnit :=
   Subsingleton.intro PUnit.subsingleton