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