C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (yoneda.obj J) ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
h : Functor.PreservesEpimorphisms (preadditiveYonedaObj J ⋙ forget (ModuleCat (End J)))
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)

case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J) → Functor.PreservesEpimorphisms (yoneda.obj J)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (yoneda.obj J) ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
refine'
  ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms => _, _⟩
no goals
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
h : Functor.PreservesEpimorphisms (preadditiveYonedaObj J ⋙ forget (ModuleCat (End J)))
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
exact
  Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
a✝ : Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (yoneda.obj J)
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J) → Functor.PreservesEpimorphisms (yoneda.obj J)
intro
no goals
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
J : C
a✝ : Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (yoneda.obj J)
exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)