∀ (ι : 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)] [inst_3 : IsEmpty ι] (f : (i : ι) → s i),
  (PiTensorProduct.isEmptyEquiv ι) ((PiTensorProduct.tprod R) f) = 1