From 061c9b81305c65cc82c014765c9ef4dd002d8766 Mon Sep 17 00:00:00 2001
From: Amelia Livingston <101damnations@github.com>
Date: Sat, 29 Jul 2023 15:51:38 +0000
Subject: [PATCH] fix(Algebra.Category.ModuleCat.Basic): remove `CoeOut
 (Submodule R M) (ModuleCat R)` instance (#6032)

---
 Mathlib/Algebra/Category/ModuleCat/Basic.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
index fb3def99d748b..2b2fac5801945 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -379,6 +379,3 @@ theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) :
 end
 
 end ModuleCat
-
-instance (M : Type u) [AddCommGroup M] [Module R M] : CoeOut (Submodule R M) (ModuleCat R) :=
-  ⟨fun N => ModuleCat.of R N⟩