[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : Injective J
⊢ PreservesFiniteColimits (preadditiveYonedaObj J)
[PROOFSTEP]
letI := (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J).mp hP
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : Injective J
this : Functor.PreservesEpimorphisms (preadditiveYonedaObj J) :=
  Iff.mp (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J) hP
⊢ PreservesFiniteColimits (preadditiveYonedaObj J)
[PROOFSTEP]
apply Functor.preservesFiniteColimitsOfPreservesEpisAndKernels
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Injective J
[PROOFSTEP]
rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
infer_instance
