Unable to prove Matrix lemma

Stream: maths

[Jai Patel]

I was trying to prove the given lemma, however, I have not been able to do so. I was wondering what the best approach would be to solving lemmas of this form.

import Mathlib
open Matrix

def CNOT1 : Matrix (Fin 4) (Fin 4) ℂ :=
   !![1, 0, 0, 0;
      0, 1, 0, 0;
      0, 0, 0, 1;
      0, 0, 1, 0]

def CNOT2 : Matrix (Fin 4) (Fin 4) ℂ :=
   !![1, 0, 0, 0;
      0, 0, 0, 1;
      0, 0, 1, 0;
      0, 1, 0, 0]

def SWAP : Matrix (Fin 4) (Fin 4) ℂ :=
   !![1, 0, 0, 0;
      0, 0, 1, 0;
      0, 1, 0, 0;
      0, 0, 0, 1]

def identity_matrix (n : ℕ) : Matrix (Fin n) (Fin n) ℂ :=
  fun i j => if i = j then 1 else 0
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
theorem h:((CNOT1)⊗(identity_matrix 2) * (identity_matrix 2)⊗(CNOT1) * (CNOT1)⊗(identity_matrix 2) * (identity_matrix 2)⊗(CNOT1))=
  ((identity_matrix 2)⊗(SWAP) * ((CNOT2)⊗(identity_matrix 2) * (identity_matrix 2)⊗(SWAP))):= by {
   sorry
}

[Eric Wieser]

I think you'll have an easier time using 1 instead of identity_matrix