no goals
C : Type u
inst✝¹ : Category C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ arrow (equalizerSubobject f g) ≫ f = arrow (equalizerSubobject f g) ≫ g
rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]