Theorem: cycleMin_eq_cycleMin_apply_inv (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ CycleMin π x = CycleMin π (π⁻¹ x)
Tactic:
rw [cycleMin_eq_cycleMin_apply (x := (π⁻¹ x)), Equiv.Perm.apply_inv_self]
State after:
no goals