The noncomm_ring tactic #

Solve goals in not necessarily commutative rings.

This tactic is rudimentary, but useful for solving simple goals in noncommutative rings. One glaring flaw is that numeric powers are unfolded entirely with pow_succ and can easily exceed the maximum recursion depth.

noncomm_ring is just a simp only [some lemmas] followed by abel. It automatically uses abel1 to close the goal, and if that doesn't succeed, defaults to abel_nf.

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
Instances For