Dual kron

lemma dual_kron {A B C D : Type*} [Fintype A] [Fintype B] [Fintype C] [Fintype D]    [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]    (M : MatrixMap A B 𝕜) (N : MatrixMap C D 𝕜) :    (M ⊗ₖₘ N).dual = M.dual ⊗ₖₘ N.dual := by  have h_trace : ∀ (X : Matrix (A × C) (A × C) 𝕜) (Y : Matrix (B × D) (B × D) 𝕜), ( (M ⊗ₖₘ N) X * Y ).trace = ( X * (M.dual ⊗ₖₘ N.dual) Y ).trace := by    -- By definition of dual, we know that $(M x1 * y1).trace = (x1 * M.dual y1).trace$ and $(N x2 * y2).trace = (x2 * N.dual y2).trace$.    have h_dual : ∀ (x1 : Matrix A A 𝕜) (y1 : Matrix B B 𝕜), (M x1 * y1).trace = (x1 * M.dual y1).trace := by      intro x1 y1      convert MatrixMap.Dual.trace_eq M x1 y1 using 1    have h_dual_N : ∀ (x2 : Matrix C C 𝕜) (y2 : Matrix D D 𝕜), (N x2 * y2).trace = (x2 * N.dual y2).trace := by      exact fun x2 y2 => MatrixMap.Dual.trace_eq N x2 y2;    intro X Y;    -- By definition of Kronecker product, we can write X and Y as sums of Kronecker products.    obtain ⟨X_sum, hX_sum⟩ : ∃ X_sum : Finset (Matrix A A 𝕜 × Matrix C C 𝕜), X = ∑ p ∈ X_sum, (Matrix.kroneckerMap (fun a b => a * b) p.1 p.2) := by      refine' ⟨ Finset.univ.image fun p : A × A × C × C => ( Matrix.of fun i j => if i = p.1 ∧ j = p.2.1 then X ( p.1, p.2.2.1 ) ( p.2.1, p.2.2.2 ) else 0, Matrix.of fun i j => if i = p.2.2.1 ∧ j = p.2.2.2 then 1 else 0 ), _ ⟩;      ext ⟨a, c⟩ ⟨a', c'⟩;      rw [ Finset.sum_apply, Finset.sum_apply ];      rw [ Finset.sum_eq_single ( ( Matrix.of fun i j => if i = a ∧ j = a' then X ( a, c ) ( a', c' ) else 0, Matrix.of fun i j => if i = c ∧ j = c' then 1 else 0 ) ) ] <;> simp;      · intro a_1 b x x_1 x_2 x_3 a_2 a_3 a_4        subst a_3 a_2        contrapose! a_4; aesop;      · exact fun h => False.elim ( h a a' c c' ( by ext i j; aesop ) ( by ext i j; aesop ) )    obtain ⟨Y_sum, hY_sum⟩ : ∃ Y_sum : Finset (Matrix B B 𝕜 × Matrix D D 𝕜), Y = ∑ p ∈ Y_sum, (Matrix.kroneckerMap (fun a b => a * b) p.1 p.2) := by      use Finset.image (fun p => (Matrix.of (fun i j => Y (i, p.1) (j, p.2)), Matrix.of (fun i j => if i = p.1 ∧ j = p.2 then 1 else 0))) (Finset.univ : Finset (D × D));      ext ⟨i, j⟩ ⟨k, l⟩; simp [ Matrix.kroneckerMap ] ;      rw [ Finset.sum_image ] <;> simp [ Matrix.sum_apply ];      · rw [ Finset.sum_eq_single ( j, l ) ] <;> aesop;      · intro p q h        subst hX_sum        simp_all only [Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq]        obtain ⟨fst, snd⟩ := p        obtain ⟨fst_1, snd_1⟩ := q        obtain ⟨left, right⟩ := h        simp_all only [Prod.mk.injEq]        apply And.intro        · have := congr_fun ( congr_fun right fst ) snd; aesop;        · replace right := congr_fun ( congr_fun right fst ) snd; aesop;    -- By linearity of the trace and the properties of the Kronecker product, we can expand both sides of the equation.    have h_expand : ∀ (x1 y1 : Matrix A A 𝕜) (x2 y2 : Matrix C C 𝕜) (x3 y3 : Matrix B B 𝕜) (x4 y4 : Matrix D D 𝕜), ( (M ⊗ₖₘ N) (Matrix.kroneckerMap (fun a b => a * b) x1 x2) * Matrix.kroneckerMap (fun a b => a * b) x3 x4 ).trace = ( Matrix.kroneckerMap (fun a b => a * b) x1 x2 * (M.dual ⊗ₖₘ N.dual) (Matrix.kroneckerMap (fun a b => a * b) x3 x4) ).trace := by      intro x1 y1 x2 y2 x3 y3 x4 y4      simp [MatrixMap.kron_map_of_kron_state]      convert congr_arg₂ ( · * · ) ( h_dual x1 x3 ) ( h_dual_N x2 x4 ) using 1 <;> simp [ Matrix.trace, Matrix.mul_apply, Matrix.kroneckerMap_apply ]      · simp only [Finset.sum_sigma', Finset.sum_mul _ _ _, Finset.mul_sum];        refine' Finset.sum_bij ( fun x _ => ⟨ ⟨ x.fst.1, x.snd.1 ⟩, ⟨ x.fst.2, x.snd.2 ⟩ ⟩ ) _ _ _ _ <;> simp [ mul_assoc, mul_comm, mul_left_comm ];        · bound;        · exact fun b => ⟨ _, _, _, _, rfl ⟩;      · simp only [mul_assoc, Finset.mul_sum _ _ _, Finset.sum_mul];        simp only [← Finset.sum_product', mul_left_comm];        refine' Finset.sum_bij ( fun x _ => ( x.1.2, x.2.2, x.1.1, x.2.1 ) ) _ _ _ _ <;> simp;    simp_all [ Matrix.trace_sum, Finset.sum_mul _ _ _ ];    simp [Matrix.mul_sum, h_expand]  apply dual_unique; assumption;