∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (self : CategoryTheory.Limits.ImageMap sq),
  CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right