case w
C : Type u
inst✝³ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage f ≫ (compIso f g).hom ≫ ι (f ≫ g) = factorThruImage f ≫ ι f ≫ g
C : Type u
inst✝³ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ (compIso f g).hom ≫ ι (f ≫ g) = ι f ≫ g
ext
no goals
case w
C : Type u
inst✝³ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage f ≫ (compIso f g).hom ≫ ι (f ≫ g) = factorThruImage f ≫ ι f ≫ g
simp [image.compIso]