no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q R : C
f : Q ⟶ R
a : P ⟶ Q
h : a ≫ f = 0
⊢ pseudoApply f (Quot.mk (PseudoEqual Q) (Over.mk a)) = 0
simp [over_coe_def, pseudoApply_mk', Over.coe_hom, h]