Lean4
/-- `mono` applies monotonicity rules and local hypotheses repetitively. For example,
```lean
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z := by
mono
```
-/
@[tactic_parser 1000]
public meta def mono : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Monotonicity.mono 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "mono" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "*")))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Mathlib.Tactic.Monotonicity.mono.side)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with ")
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝)
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt) (ParserDescr.cat✝ `term 0)) ","
(ParserDescr.symbol✝ ", ") Bool.false✝))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ")
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝)
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt) Lean.Parser.Tactic.simpArg) ","
(ParserDescr.symbol✝ ", ") Bool.false✝))))
