∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : Cᵒᵖ),
  ((CategoryTheory.linearYoneda R C).map f).app Y =
    ModuleCat.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)