rw [Finset.sum_comm]
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
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