commutator between tensor products

I am interested in some quantum mechanical calculations in Mathematica. I am working with a tensor product of Hilbert spaces $$\mathcal H = \mathcal H_1\otimes \mathcal H_2$$. I would like to implement the following operator rule, to be applied in any occurrence in my calculations: $$[\hat A_1,\hat B_1\otimes \hat A_2] = [\hat A_1,\hat B_1]\otimes \hat A_2$$ where the indices refer to the two Hilber spaces. Which is the most convenient way to do so?

Square brackets are a reserved symbol. So, you must choose another symbol without inbuilt meaning, e.g. AngleBrackets. The CircleTimes is available. If you now want to define the rule above you say:

\[LeftAngleBracket]A1_ ,
B1_ \[CircleTimes] A2_\[RightAngleBracket] = \[LeftAngleBracket]A1,
B1\[RightAngleBracket] \[CircleTimes]A2


you then get:

\[LeftAngleBracket]x, y \[CircleTimes]  z\[RightAngleBracket]


This looks better formatted:

Note: Any other algebraic rule you want, must be specified by you