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.

theorem Mathlib.Tactic.NoncommRing.nat_lit_mul_eq_nsmul {R : Type u_1} [NonAssocSemiring R] (r : R) (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n * r = OfNat.ofNat n • r

theorem Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul {R : Type u_1} [NonAssocSemiring R] (r : R) (n : ℕ) [n.AtLeastTwo] : r * OfNat.ofNat n = OfNat.ofNat n • r

def Mathlib.Tactic.NoncommRing.noncomm_ring : Lean.ParserDescr

noncomm_ring simplifies expressions in not-necessarily-commutative rings in the main goal then tries closing it by "cheap" (reducible) rfl. This tactic supports the operators +, *, -, ^ and • (for scalar multiplication by natural numbers or integers).

If the ring is commutative, prefer the ring tactic instead, which is more powerful and efficient. The tactic is implemented as a combination of simp only [...] and abel. The precise invocation of simp only can be customized using the options listed below.

Limitation: numeric powers are unfolded entirely with pow_succ and can easily exceed the maximum recursion depth.

• noncomm_ring [h] adds the term h as simplification lemma, rewriting from left to right. Multiple arguments can be combined as noncomm_ring [h₁, ..., hₙ].
• noncomm_ring [← h] adds the term h as simplification lemma, rewriting from right to left.
• noncomm_ring [*] simplifies using all hypotheses in the local context.
• noncomm_ring (config := cfg) uses cfg as configuration for the simplification step. See Lean.Meta.Simp.Config for more details.
• noncomm_ring (discharger := tac) uses the tactic sequence tac to discharge assumptions to the simplification lemmas. This only applies to user-supplied lemmas, since the default lemmas used by noncomm_ring do not require a discharger.

Example:

example {R : Type*} [Ring R] (a b c : R) : a * (b + c + c - b) = 2 * a * c := by
  noncomm_ring

We register noncomm_ring with the hint tactic.