∀ {R : Type u_1} [inst : CommRing R] (M N P : ModuleCat R)
  (f : (CategoryTheory.MonoidalCategory.tensorLeft M).obj N ⟶ P),
  (fun f =>
        CategoryTheory.CategoryStruct.comp (β_ M N).hom (ModuleCat.ofHom (TensorProduct.lift (ModuleCat.Hom.hom₂ f))))
      ((fun f =>
          ModuleCat.ofHom₂
            ((TensorProduct.mk R ↑N ↑M).compr₂ (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (β_ N M).hom f))))
        f) =
    f