Help with a type matching issue in Lean 4

Stream: lean4

[Anirudh Suresh]

import Mathlib
open scoped Matrix

def tensor_product_2 {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ)
  (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
(Matrix.kroneckerMap (fun (a:ℂ) (b:ℂ) => a*b) A B).reindex finProdFinEquiv finProdFinEquiv

infixl:80 " ⊗ " => tensor_product_2

def I1 : Matrix (Fin 1) (Fin 1) ℂ := !![1]

noncomputable def tensor_product_list (L : List (Matrix (Fin 2) (Fin 2) ℂ))
  : Matrix (Fin (2^(L.length))) (Fin (2^(L.length))) ℂ :=
match L with
| []      => I1
| (x::xs) => (x ⊗ (tensor_product_list xs))

I am getting a type error in my code. However, this error no longer exists when i write

((tensor_product_list xs)⊗ x)

However, this does not work for me because tensor product is not commutative. How should I proceed to avoid this type error?

[Henrik Böving]

For example like this:

noncomputable def tensor_product_list (L : List (Matrix (Fin 2) (Fin 2) ℂ))
  : Matrix (Fin (2^(L.length))) (Fin (2^(L.length))) ℂ :=
match L with
| []      => I1
| (x::xs) =>
  let foo := (x ⊗ (tensor_product_list xs))
  have : 2 ^ (x :: xs).length = 2 * 2 ^ xs.length := by simp [Nat.pow_succ, Nat.mul_comm 2 _]
  this ▸ foo