no goals
C : Type u₁
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
inst✝² : HasImages Cᵒᵖ
inst✝¹ : HasEqualizers Cᵒᵖ
J Q R S : C
inst✝ : Injective J
h : R ⟶ J
f : Q ⟶ R
g : R ⟶ S
hgf : Exact g.op f.op
w : f ≫ h = 0
⊢ g ≫ desc h f g hgf w = h
convert congr_arg Quiver.Hom.unop (Exact.lift_comp h.op g.op f.op hgf (congrArg Quiver.Hom.op w))