no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ 𝟙 (pullback f q.hom) ≫ ((fun g => app f g) (Over.mk pullback.fst)).hom = pullback.snd ≫ q.hom
rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]