chore(*): 3 unrelated small changes (#4732)
* fix universe levels in `equiv.set.compl`: by default Lean uses some
`max` universes both for `α` and `β`, and it backfires when one tries
to apply it.
* add `nat.mul_factorial_pred`;
* add instance `fixed_points.decidable`.
Part of #4731
