Theorem: card_cycleAtTo_le (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ (CycleAtTo π a x).card ≤ a
Tactic:
convert Finset.card_image_le
State after:
case h.e'_4
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ a = (Iio a).card

State before:
case h.e'_4
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
⊢ a = (Iio a).card
Tactic:
exact (Nat.card_Iio _).symm
State after:
no goals