Lean4
/-- The tactic `reduce_mod_char` looks for numeric expressions in characteristic `p`
and reduces these to lie between `0` and `p`.
For example:
```
example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char
```
It also handles negation, turning it into multiplication by `p - 1`,
and similarly subtraction.
This tactic uses the type of the subexpression to figure out if it is indeed of positive
characteristic, for improved performance compared to trying to synthesise a `CharP` instance.
The variant `reduce_mod_char!` also tries to use `CharP R n` hypotheses in the context.
(Limitations of the typeclass system mean the tactic can't search for a `CharP R n` instance if
`n` is not yet known; use `have : CharP R n := inferInstance; reduce_mod_char!` as a workaround.)
-/
@[tactic_parser 1000]
public meta def reduce_mod_char : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Tactic.ReduceModChar.reduce_mod_char 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "reduce_mod_char" false✝)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
