Theorem: cycleMin_of_fixed (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
h : Function.IsFixedPt (⇑π) x
⊢ CycleMin π x = x
Tactic:
simp_rw [cycleMin_eq_min_cycleAtTo, π.cycleOf_eq_one_iff.mpr h, orderOf_one,
  cycleAtTo_one, min'_singleton]
State after:
no goals