∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left)
  (r : f.right ≅ g.right)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
      CategoryTheory.Arrow.isoMk._auto_1),
  (CategoryTheory.Arrow.isoMk l r h).hom.left = l.hom