case h
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
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ arrow (imageSubobject (Arrow.mk g).hom) =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ arrow (imageSubobject (Arrow.mk g).hom)
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
⊢ image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv = (imageSubobjectIso f).inv ≫ imageSubobjectMap sq
ext
no goals
case h
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
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ arrow (imageSubobject (Arrow.mk g).hom) =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ arrow (imageSubobject (Arrow.mk g).hom)
simpa using image.map_ι sq