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