Theorem: MatrixCookbook.eq_520 (MatrixCookbook/10FunctionsAndOperators.lean)

State before:
ι : Type ?u.49154
R : Type u_3
l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.49172
r : Type ?u.49175
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l m R
X : Matrix m n R
B : Matrix n p R
⊢ vec (A * X * B) = kroneckerMap (fun x x_1 => x * x_1) Bᵀ A * vec X
Tactic:
ext ⟨k, l⟩
State after:
case a.mk
ι : Type ?u.49154
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.49172
r : Type ?u.49175
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix n p R
k : p
l : l✝
j✝ : Unit
⊢ vec (A * X * B) (k, l) j✝ = (kroneckerMap (fun x x_1 => x * x_1) Bᵀ A * vec X) (k, l) j✝

State before:
case a.mk
ι : Type ?u.49154
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.49172
r : Type ?u.49175
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix n p R
k : p
l : l✝
j✝ : Unit
⊢ vec (A * X * B) (k, l) j✝ = (kroneckerMap (fun x x_1 => x * x_1) Bᵀ A * vec X) (k, l) j✝
Tactic:
simp_rw [vec, Matrix.mul_apply, Matrix.kroneckerMap_apply, col_apply, Finset.sum_mul,
  transpose_apply, ← Finset.univ_product_univ, Finset.sum_product, mul_right_comm _ _ (B _ _),
  mul_comm _ (B _ _)]
State after:
no goals