C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyonedaObj G.op ⋙ forget₂ (ModuleCat (End G.op)) AddCommGroupCat) ↔
    Faithful (preadditiveCoyonedaObj G.op)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ Faithful (preadditiveCoyonedaObj G.op)
rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyonedaObj G.op ⋙ forget₂ (ModuleCat (End G.op)) AddCommGroupCat) ↔
    Faithful (preadditiveCoyonedaObj G.op)
exact ⟨fun h => Faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => Faithful.comp _ _⟩