Theorem: cycleAt_gt_cycleAtTo_lt_orderOf_cycleOf (Controlbits/Cycles.lean)

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

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a < orderOf (π.cycleOf x)
⊢ CycleAtTo π a x ⊂ CycleAtTo π (orderOf (π.cycleOf x)) x
Tactic:
exact cycleAtTo_strict_mono_lt_of_lt_lt_orderOf h h
State after:
no goals