∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Subsingleton ι] (i₀ : ι),
  { toFun := fun x => (PiTensorProduct.tprod R) (Function.update 0 i₀ x), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      PiTensorProduct.lift { toFun := fun f => f i₀, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    LinearMap.id