Lean4
/-- Simplification tactic for expressions in the language of commutative (semi)rings,
which rewrites all ring expressions into a normal form.
* `ring_nf!` will use a more aggressive reducibility setting to identify atoms.
* `ring_nf (config := cfg)` allows for additional configuration:
* `red`: the reducibility setting (overridden by `!`)
* `zetaDelta`: if true, local let variables can be unfolded (overridden by `!`)
* `recursive`: if true, `ring_nf` will also recurse into atoms
* `ring_nf` works as both a tactic and a conv tactic.
In tactic mode, `ring_nf at h` can be used to rewrite in a hypothesis.
This can be used non-terminally to normalize ring expressions in the goal such as
`⊢ P (x + x + x)` ~> `⊢ P (x * 3)`, as well as being able to prove some equations that
`ring` cannot because they involve ring reasoning inside a subterm, such as
`sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
-/
@[tactic_parser 1000]
public meta def ringNF : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.RingNF.ringNF 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "ring_nf" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
