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