monotonicity performs one compositional step solving monotone goals,
using lemma tagged with @[partial_fixpoint_monotone].
This tactic is mostly used internally by lean in partial_fixpoint definitions, but
can be useful on its own for debugging or when proving new @[partial_fixpoint_monotone] lemmas.
Equations
- Lean.Order.monotonicity = Lean.ParserDescr.node `Lean.Order.monotonicity 1024 (Lean.ParserDescr.nonReservedSymbol "monotonicity" false)