no goals
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ (factorThru P (f + g) w - factorThru P g wg) ≫ MonoOver.arrow (representative.obj P) = f
simp