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

State before:
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
⊢ row a * X * B * Xᵀ * col c = (vec X)ᵀ * kroneckerMap (fun x x_1 => x * x_1) Bᵀ (col c * row a) * vec X
Tactic:
ext ⟨i, j⟩
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ (row a * X * B * Xᵀ * col c) PUnit.unit j✝ =
    ((vec X)ᵀ * kroneckerMap (fun x x_1 => x * x_1) Bᵀ (col c * row a) * vec X) PUnit.unit j✝

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ (row a * X * B * Xᵀ * col c) PUnit.unit j✝ =
    ((vec X)ᵀ * kroneckerMap (fun x x_1 => x * x_1) Bᵀ (col c * row a) * vec X) PUnit.unit j✝
Tactic:
simp only [vec, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum, Matrix.kroneckerMap_apply,
  transpose_apply, Matrix.row_apply, Matrix.col_apply, Fintype.sum_unique]
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : m, ∑ x_1 : n, ∑ x_2 : n, ∑ i : m, a i * X i x_2 * B x_2 x_1 * X x x_1 * c x =
    ∑ x : n × m, ∑ i : n × m, X i.2 i.1 * (B x.1 i.1 * (c i.2 * a x.2)) * X x.2 x.1

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : m, ∑ x_1 : n, ∑ x_2 : n, ∑ i : m, a i * X i x_2 * B x_2 x_1 * X x x_1 * c x =
    ∑ x : n × m, ∑ i : n × m, X i.2 i.1 * (B x.1 i.1 * (c i.2 * a x.2)) * X x.2 x.1
Tactic:
simp_rw [← Finset.univ_product_univ, Finset.sum_product, @Finset.sum_comm n _ m]
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x
Tactic:
rw [Finset.sum_comm]
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ y : n, ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ y : n, ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x
Tactic:
refine' Finset.sum_congr rfl fun k _ => _
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝ : k ∈ Finset.univ
⊢ ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i k * B k x * X x_1 x * c x_1 =
    ∑ y : n, ∑ x : m, ∑ x_1 : m, X x_1 y * (B k y * (c x_1 * a x)) * X x k

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝ : k ∈ Finset.univ
⊢ ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i k * B k x * X x_1 x * c x_1 =
    ∑ y : n, ∑ x : m, ∑ x_1 : m, X x_1 y * (B k y * (c x_1 * a x)) * X x k
Tactic:
refine' Finset.sum_congr rfl fun l _ => _
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ x : m, ∑ i : m, a i * X i k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ x : m, ∑ i : m, a i * X i k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k
Tactic:
rw [Finset.sum_comm]
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ y : m, ∑ x : m, a y * X y k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ y : m, ∑ x : m, a y * X y k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k
Tactic:
refine' Finset.sum_congr rfl fun kk _ => _
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝² : k ∈ Finset.univ
l : n
x✝¹ : l ∈ Finset.univ
kk : m
x✝ : kk ∈ Finset.univ
⊢ ∑ x : m, a kk * X kk k * B k l * X x l * c x = ∑ x : m, X x l * (B k l * (c x * a kk)) * X kk k

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝² : k ∈ Finset.univ
l : n
x✝¹ : l ∈ Finset.univ
kk : m
x✝ : kk ∈ Finset.univ
⊢ ∑ x : m, a kk * X kk k * B k l * X x l * c x = ∑ x : m, X x l * (B k l * (c x * a kk)) * X kk k
Tactic:
refine' Finset.sum_congr rfl fun ll _ => _
State after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝³ : k ∈ Finset.univ
l : n
x✝² : l ∈ Finset.univ
kk : m
x✝¹ : kk ∈ Finset.univ
ll : m
x✝ : ll ∈ Finset.univ
⊢ a kk * X kk k * B k l * X ll l * c ll = X ll l * (B k l * (c ll * a kk)) * X kk k

State before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
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 : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝³ : k ∈ Finset.univ
l : n
x✝² : l ∈ Finset.univ
kk : m
x✝¹ : kk ∈ Finset.univ
ll : m
x✝ : ll ∈ Finset.univ
⊢ a kk * X kk k * B k l * X ll l * c ll = X ll l * (B k l * (c ll * a kk)) * X kk k
Tactic:
ring
State after:
no goals