From e841f167383ddff1c32ae9dadfce5263fd795645 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Mar 2021 19:50:11 -0800
Subject: [PATCH] fix: typo in theorem

`()` is `Unit`
---
 src/Init/Core.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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