From 757e593ea428bb1198609962946f561027cfe7e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 13 May 2024 14:38:41 +0200
Subject: [PATCH] fixing the build

---
 Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean
index 947671445a5df..80d80075b9e8a 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean
@@ -24,12 +24,12 @@ variable {C : Type u₁} [Category.{v₁} C] (R : Cᵒᵖ ⥤ RingCat.{u})
 noncomputable instance : NormalEpiCategory (PresheafOfModules.{v} R) where
   normalEpiOfEpi p _ := NormalEpi.mk _ (kernel.ι p)  (kernel.condition _)
     (evaluationJointlyReflectsColimits _ _ (fun _ =>
-      Abelian.isColimitMapCoconeOfCokernelCoforkOfπKernelConditionOfEpi _ _))
+      Abelian.isColimitMapCoconeOfCokernelCoforkOfπ _ _))
 
 noncomputable instance : NormalMonoCategory (PresheafOfModules.{v} R) where
   normalMonoOfMono i _ := NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
     (evaluationJointlyReflectsLimits _ _ (fun _ =>
-      Abelian.isLimitMapConeOfKernelForkOfιCokernelConditionOfMono _ _))
+      Abelian.isLimitMapConeOfKernelForkOfι _ _))
 
 noncomputable instance : Abelian (PresheafOfModules.{v} R) where