∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_4} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_5}
  [inst_3 : DecidableEq ι] (pn : TensorProduct R (ι →₀ R) N) (i : ι),
  ((TensorProduct.finsuppScalarLeft R N ι) pn) i = (TensorProduct.lid R N) ((LinearMap.rTensor N (Finsupp.lapply i)) pn)