C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ f = 0
rw [← Category.id_comp f]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0
exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))