For any n-order matrix A, B, H
$[A, B] \stackrel{\text { def }}{=} A B-B A$
Try to prove：
(1) $\left[k_{1} \boldsymbol{A}+k_{2} \boldsymbol{B}, \boldsymbol{H}\right]=k_{1}[\boldsymbol{A}, \boldsymbol{H}]+k_{2}[\boldsymbol{B}, \boldsymbol{H}]$
Clear["Global`*"];
$Assumptions = (A | B | H) \[Element] Matrices[{n, n}];
$Assumptions = Element[Subscript[k, 1] | Subscript[k, 2], Reals];
f[x_, y_] := x . y - y . x;
G = Subscript[k, 1]*A + Subscript[k, 2]*B;
TensorReduce[
f[G, H] == Subscript[k, 1]*f[A, H] + Subscript[k, 2]*f[B, H]]
$-\mathrm{H} \cdot\left(\mathrm{A} \mathrm{k}_{1}+\mathrm{B} \mathrm{k}_{2}\right)+\left(\mathrm{A} \mathrm{k}_{1}+\mathrm{B} \mathrm{k}_{2}\right) \cdot \mathrm{H}==(\mathrm{A} \cdot \mathrm{H}-\mathrm{H} \cdot \mathrm{A}) \mathrm{k}_{1}+(\mathrm{B} \cdot \mathrm{H}-\mathrm{H} \cdot \mathrm{B}) \mathrm{k}_{2}$
Failed.
(2) $[A, B]=-[B, A]$
Clear["Global`*"];
$Assumptions = Element[A | B, Matrices[{n, n}]];
f[x_, y_] := x . y - y . x;
TensorReduce[f[A, B] == -f[B, A]]
True
(3) $[A,[B, H]]+[B,[H, A]]+[H,[A, B]]=0$
Clear["Global`*"];
$Assumptions = Element[A | B | H, Matrices[{n, n}]];
f[x_, y_] := x . y - y . x;
TensorReduce[f[A, f[B, H]] + f[B, f[H, A]] + f[H, f[A, B]] == 0]
True
How can I prove question (1)?
