∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X