C : Type u
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = arrow (imageSubobject f) ≫ sq.right
C : Type u
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ imageSubobjectMap sq ≫ arrow (imageSubobject g) = arrow (imageSubobject f) ≫ sq.right
simp only [imageSubobjectMap, Category.assoc, imageSubobject_arrow']
no goals
C : Type u
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = arrow (imageSubobject f) ≫ sq.right
erw [image.map_ι, ← Category.assoc, imageSubobject_arrow]