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.