Theorem: cycleAt_eq_cycleAtTo_ge_orderOf_cycleOf (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAt π x = CycleAtTo π a x
Tactic:
refine le_antisymm ?_ ?_
State after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAt π x ≤ CycleAtTo π a x

case refine_2
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π a x ≤ CycleAt π x

State before:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAt π x ≤ CycleAtTo π a x
Tactic:
rw [cycleAt_eq_cycleAtTo_orderOf_cycleOf]
State after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π (orderOf (π.cycleOf x)) x ≤ CycleAtTo π a x

State before:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π (orderOf (π.cycleOf x)) x ≤ CycleAtTo π a x
Tactic:
exact cycleAtTo_of_mono ha
State after:
no goals

State before:
case refine_2
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
a : ℕ
ha : orderOf (π.cycleOf x) ≤ a
⊢ CycleAtTo π a x ≤ CycleAt π x
Tactic:
exact cycleAtTo_subset_cycleAt
State after:
no goals