∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)],
  PiTensorProduct.piTensorHomMap =
    ↑PiTensorProduct.lift ∘ₗ PiTensorProduct.lift (MultilinearMap.piLinearMap (PiTensorProduct.tprod R))