∀ (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ),
  ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a