mathlib documentation

tactic.noncomm_ring

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