Theorem: cycleAtTo_card_eq_of_le_orderOf_cycleOf (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ (CycleAtTo π a x).card = a
Tactic:
nth_rewrite 2 [← Nat.card_Iio a]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ (CycleAtTo π a x).card = (Iio a).card

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ (CycleAtTo π a x).card = (Iio a).card
Tactic:
apply Finset.card_image_iff.mpr
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ Set.InjOn (fun k => (π ^ k) x) ↑(Iio a)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
⊢ Set.InjOn (fun k => (π ^ k) x) ↑(Iio a)
Tactic:
intros b hb c hc hbc
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b : ℕ
hb : b ∈ ↑(Iio a)
c : ℕ
hc : c ∈ ↑(Iio a)
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
⊢ b = c

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b : ℕ
hb : b ∈ ↑(Iio a)
c : ℕ
hc : c ∈ ↑(Iio a)
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
⊢ b = c
Tactic:
simp_rw [coe_Iio, Set.mem_Iio] at hb hc
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b c : ℕ
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
hb : b < a
hc : c < a
⊢ b = c

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
a : ℕ
x : α
h : a ≤ orderOf (π.cycleOf x)
b c : ℕ
hbc : (fun k => (π ^ k) x) b = (fun k => (π ^ k) x) c
hb : b < a
hc : c < a
⊢ b = c
Tactic:
exact π.pow_apply_injOn_Iio_orderOf_cycleOf (lt_of_lt_of_le hb h) (lt_of_lt_of_le hc h) hbc
State after:
no goals