QuantumInfo.ForMathlib.Tactic.Commutes

The tactic `commutes` is designed to automatically discharge goals involving the `Commute` proposition, $ab = ba$, for elements $a, b$ in a ring or algebra. It utilizes `aesop` to perform structural recursion on the expressions and applies basic normalization of ring operations to establish if two elements commute.

The tactic `commutes?` is a variant of the `commutes` tactic used to discharge goals involving the `Commute` relation ($xy = yx$). Unlike the standard version, this variant generates and suggests a proof script that the user can use to replace the tactic call.