ι : Type ?u.3070884
α : Type u_1
β : Type ?u.3070890
inst✝² inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ IsCycleOn (List.formPerm (toList s)) ↑s
ι : Type ?u.3070884
α : Type u_1
β : Type ?u.3070890
inst✝² inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ∃ f, IsCycleOn f ↑s ∧ support f ⊆ s
refine'
  ⟨s.toList.formPerm, _, fun x hx => by
    simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)⟩
case h.e'_3
ι : Type ?u.3070884
α : Type u_1
β : Type ?u.3070890
inst✝² inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ↑s = {a | a ∈ toList s}
ι : Type ?u.3070884
α : Type u_1
β : Type ?u.3070890
inst✝² inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ IsCycleOn (List.formPerm (toList s)) ↑s
convert s.nodup_toList.isCycleOn_formPerm
no goals
case h.e'_3
ι : Type ?u.3070884
α : Type u_1
β : Type ?u.3070890
inst✝² inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ↑s = {a | a ∈ toList s}
simp
no goals
ι : Type ?u.3070884
α : Type u_1
β : Type ?u.3070890
inst✝² inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
x : α
hx : x ∈ support (List.formPerm (toList s))
⊢ x ∈ s
simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)