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

src/data/equiv/basic.lean

@@ -1407,8 +1407,9 @@ calc  (s ∪ t : set α) ⊕ (s ∩ t : set α)
 /-- Given an equivalence `e₀` between sets `s : set α` and `t : set β`, the set of equivalences
 `e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences
 between `sᶜ` and `tᶜ`. -/
-protected def compl {α β : Type*} {s : set α} {t : set β} [decidable_pred s] [decidable_pred t]
-  (e₀ : s ≃ t) : {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
+protected def compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_pred s]
+  [decidable_pred t] (e₀ : s ≃ t) :
+  {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
 { to_fun := λ e, subtype_congr e
     (λ a, not_congr $ iff.symm $ maps_to.mem_iff
       (maps_to_iff_exists_map_subtype.2 ⟨e₀, e.2⟩)

src/data/nat/factorial.lean

@@ -25,6 +25,12 @@ localized "notation n `!`:10000 := nat.factorial n" in nat
 
 @[simp] theorem factorial_one : 1! = 1 := rfl
 
+theorem mul_factorial_pred (hn : 0 < n) : n * (n - 1)! = n! :=
+have n - 1 + 1 = n, from nat.sub_add_cancel (succ_le_of_lt hn),
+calc n * (n - 1)! = (n - 1 + 1) * (n - 1)! : by rw this
+... = (n - 1 + 1)! : rfl
+... = n! : by rw this
+
 theorem factorial_pos : ∀ n, 0 < n!
 | 0        := zero_lt_one
 | (succ n) := mul_pos (succ_pos _) (factorial_pos n)

src/dynamics/fixed_points/basic.lean

@@ -73,6 +73,10 @@ end is_fixed_pt
 /-- The set of fixed points of a map `f : α → α`. -/
 def fixed_points (f : α → α) : set α := {x : α | is_fixed_pt f x}
 
+instance fixed_points.decidable [decidable_eq α] (f : α → α) (x : α) :
+  decidable (x ∈ fixed_points f) :=
+is_fixed_pt.decidable
+
 @[simp] lemma mem_fixed_points : x ∈ fixed_points f ↔ is_fixed_pt f x := iff.rfl
 
 /-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points