refine' Finset.sum_congr rfl fun ll _ => _
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
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