Theorem: le_cycleMin_iff (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
z x : α
⊢ z ≤ CycleMin π x ↔ ∀ (y : α), π.SameCycle x y → z ≤ y
Tactic:
simp_rw [cycleMin_def, Finset.le_min'_iff, mem_cycleAt_iff]
State after:
no goals