no goals
C : Type u
inst✝¹ : Category C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : Factors (equalizerSubobject f g) h
⊢ h ≫ f = h ≫ g
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
  Category.assoc]