Theorem: le_cycleMin (Controlbits/Cycles.lean)

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

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x z : α
h : ∀ (y : α), π.SameCycle x y → z ≤ y
⊢ ∀ (y : α), π.SameCycle x y → z ≤ y
Tactic:
exact h
State after:
no goals