Lean4
/-- A tactic for simplifying identities in not-necessarily-commutative rings.
An example:
```lean
example {R : Type*} [Ring R] (a b c : R) : a * (b + c + c - b) = 2 * a * c := by
noncomm_ring
```
You can use `noncomm_ring [h]` to also simplify using `h`.
-/
@[tactic_parser 1000]
public meta def noncomm_ring : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.NoncommRing.noncomm_ring 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "noncomm_ring" false✝)
Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.discharger))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝)
(ParserDescr.binary✝ `orelse Lean.Parser.Tactic.simpStar
(ParserDescr.binary✝ `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma))
"," (ParserDescr.symbol✝ ", ") Bool.true✝))
(ParserDescr.symbol✝ "]"))))
