case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ↑f x = x
⊢ orderOf (cycleOf f x) ∣ orderOf f

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ orderOf (cycleOf f x) ∣ orderOf f
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
⊢ orderOf (cycleOf f x) ∣ orderOf f
by_cases hx : f x = x
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx✝ : ↑f x = x
hx : cycleOf f x = 1
⊢ orderOf (cycleOf f x) ∣ orderOf f
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ↑f x = x
⊢ orderOf (cycleOf f x) ∣ orderOf f
rw [← cycleOf_eq_one_iff] at hx
no goals
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx✝ : ↑f x = x
hx : cycleOf f x = 1
⊢ orderOf (cycleOf f x) ∣ orderOf f
simp [hx]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ orderOf (cycleOf f x) ∈ cycleType f
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ orderOf (cycleOf f x) ∣ orderOf f
refine dvd_of_mem_cycleType ?_
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ ∃ a, a ∈ (cycleFactorsFinset f).val ∧ (Finset.card ∘ support) a = orderOf (cycleOf f x)
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ orderOf (cycleOf f x) ∈ cycleType f
rw [cycleType, Multiset.mem_map]
case neg.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ cycleOf f x ∈ (cycleFactorsFinset f).val

case neg.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ (Finset.card ∘ support) (cycleOf f x) = orderOf (cycleOf f x)
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ ∃ a, a ∈ (cycleFactorsFinset f).val ∧ (Finset.card ∘ support) a = orderOf (cycleOf f x)
refine' ⟨f.cycleOf x, _, _⟩
no goals
case neg.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ cycleOf f x ∈ (cycleFactorsFinset f).val
rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
no goals
case neg.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ (Finset.card ∘ support) (cycleOf f x) = orderOf (cycleOf f x)
simp [(isCycle_cycleOf _ hx).orderOf]