C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj P.op) ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
h : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)

case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op) → Functor.PreservesEpimorphisms (coyoneda.obj P.op)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj P.op) ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
refine' ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
    forget AddCommGroupCat).PreservesEpimorphisms => _, _⟩
no goals
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
h : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P))
    (forget _)
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
a✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
⊢ Functor.PreservesEpimorphisms (coyoneda.obj P.op)
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op) → Functor.PreservesEpimorphisms (coyoneda.obj P.op)
intro
no goals
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
P : C
a✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
⊢ Functor.PreservesEpimorphisms (coyoneda.obj P.op)
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)