From bb3fc358c92d6d081a6e30f6ab9dfeb9de17997f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 Apr 2022 14:52:41 -0700
Subject: [PATCH] feat: add `LawfulBEq Int` instance

---
 src/Init/Data/Int/Basic.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 736ca69232..68d95ff0a1 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -170,4 +170,8 @@ protected def pow (m : Int) : Nat → Int
 instance : HPow Int Nat Int where
   hPow := Int.pow
 
+instance : LawfulBEq Int where
+  eq_of_beq a b h := by simp [BEq.beq] at h; assumption
+  rfl a := by simp [BEq.beq]
+
 end Int