C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Quotient.mk (setoid Q) (Over.mk ((Over.mk 0).hom ≫ f)) = 0
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ pseudoApply f 0 = 0
rw [pseudoZero_def, pseudoApply_mk']
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Quotient.mk (setoid Q) (Over.mk ((Over.mk 0).hom ≫ f)) = 0
simp