∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.LoopAlgebra.toFinsupp R A L = TensorProduct.equivFinsuppOfBasisLeft (AddMonoidAlgebra.basis A R)