noncomputable def lemma_23_78 (R : Type u) [CommRing R] (M A : ModuleCat R) : ((CategoryTheory.Tor (ModuleCat R) 0).obj M).obj A ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj M A