Lean4
/-- * The tactic `mod_cases h : e % 3` will perform a case disjunction on `e`.
If `e : ℤ`, then it will yield subgoals containing the assumptions
`h : e ≡ 0 [ZMOD 3]`, `h : e ≡ 1 [ZMOD 3]`, `h : e ≡ 2 [ZMOD 3]`
respectively. If `e : ℕ` instead, then it works similarly, except with
`[MOD 3]` instead of `[ZMOD 3]`.
* In general, `mod_cases h : e % n` works
when `n` is a positive numeral and `e` is an expression of type `ℕ` or `ℤ`.
* If `h` is omitted as in `mod_cases e % n`, it will be default-named `H`.
-/
@[tactic_parser 1000]
public meta def «tacticMod_cases_:_%_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.ModCases.«tacticMod_cases_:_%_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "mod_cases " false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.unary✝ `atomic (ParserDescr.binary✝ `andthen Lean.binderIdent (ParserDescr.symbol✝ ":")))))
(ParserDescr.cat✝ `term 71))
(ParserDescr.symbol✝ " % "))
(ParserDescr.const✝ `num))
