From 55ce5d570c818f16f62eaa53e344db06e7f82d68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Feb 2024 13:28:25 -0800 Subject: [PATCH] chore: add temporary workaround --- src/Init/Data/Int/DivModLemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index e477f1f8a6..19aac50aa6 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -343,5 +343,5 @@ def bmod (x : Int) (m : Nat) : Int := r - m @[simp] theorem bmod_emod : bmod x m % m = x % m := by - dsimp [bmod] + simp [bmod] -- TODO (zeta): It was `dsimp` split <;> simp [Int.sub_emod]