adapt

leanprover-community · Feb 22, 2025 · 1882fbe · 1882fbe
1 parent 19a2463
commit 1882fbe
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1707,6 +1707,7 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
 import Mathlib.CategoryTheory.Abelian.Images

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
@@ -23,10 +23,6 @@ namespace CategoryTheory.Abelian.IsGrothendieckAbelian
 
 variable {C : Type u} [Category.{v} C] {D : Type v} [SmallCategory D] (F : D ⥤ Cᵒᵖ)
 
-theorem epi_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) :
-    Epi (f ≫ g) :=
-  inferInstance
-
 namespace OppositeModuleEmbedding
 
 variable [Abelian C] [IsGrothendieckAbelian.{v} C]