no goals
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ 0
simpa only [Limits.comp_zero] using hf
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ (f - g) = 0
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg