C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyoneda.obj G.op ⋙ forget AddCommGroupCat) ↔ Faithful (preadditiveCoyoneda.obj G.op)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ Faithful (preadditiveCoyoneda.obj G.op)
rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj,
  whiskeringRight_obj_obj]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyoneda.obj G.op ⋙ forget AddCommGroupCat) ↔ Faithful (preadditiveCoyoneda.obj G.op)
exact ⟨fun h => Faithful.of_comp _ (forget AddCommGroupCat), fun h => Faithful.comp _ _⟩