tactic.noncomm_ring
source
A tactic for simplifying identities in not-necessarily-commutative rings.
An example:
example {R : Type*} [ring R] (a b c : R) : a * (b + c + c - b) = 2*a*c := by noncomm_ring