From d8047ddeb1c969784150d1dee1bc41fe0f32c179 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 25 Mar 2024 19:28:31 +0000
Subject: [PATCH] fix: change `Quotient.sound` to a `theorem` (#3765)

The result is a proof, so presumably this should not be a `def`.
---
 src/Init/Core.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 09e305af34..66d3cd2d56 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1596,7 +1596,7 @@ protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
 The analogue of `Quot.sound`: If `a` and `b` are related by the equivalence relation,
 then they have equal equivalence classes.
 -/
-def sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
+theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
   Quot.sound
 
 /--