Theorem: cycleMin_le (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π✝ : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
y : α
π : Perm α
x : α
h : π.SameCycle x y
⊢ CycleMin π x ≤ y
Tactic:
rw [cycleMin_def]
State after:
α : Type u
inst✝² : DecidableEq α
π✝ : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
y : α
π : Perm α
x : α
h : π.SameCycle x y
⊢ (CycleAt π x).min' ⋯ ≤ y

State before:
α : Type u
inst✝² : DecidableEq α
π✝ : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
y : α
π : Perm α
x : α
h : π.SameCycle x y
⊢ (CycleAt π x).min' ⋯ ≤ y
Tactic:
exact Finset.min'_le _ y (mem_cycleAt_iff.mpr h)
State after:
no goals