∀ (R : Type u_3) [inst : Ring R] (C : Type u_1) [inst_1 : CategoryTheory.Category.{u_2, u_1} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (X : C) (X_1 : Cᵒᵖ),
  ModuleCat.ofHom (CategoryTheory.Linear.leftComp R X (CategoryTheory.CategoryStruct.id X_1).unop) =
    CategoryTheory.CategoryStruct.id (ModuleCat.of R (Opposite.unop X_1 ⟶ X))