α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length (attach l)
⊢ cycleType (formPerm (attach l)) = {length l}
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length l
⊢ cycleType (formPerm (attach l)) = {length l}
rw [← length_attach] at hn
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ cycleType (formPerm (attach l)) = {length l}
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length (attach l)
⊢ cycleType (formPerm (attach l)) = {length l}
rw [← nodup_attach] at hl
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑(map (Finset.card ∘ support) [formPerm (attach l)]) = {length l}

case h0
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ prod [formPerm (attach l)] = formPerm (attach l)

case h1
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ∀ (σ : Equiv.Perm { x // x ∈ l }), σ ∈ [formPerm (attach l)] → IsCycle σ

case h2
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ Pairwise Perm.Disjoint [formPerm (attach l)]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ cycleType (formPerm (attach l)) = {length l}
rw [cycleType_eq [l.attach.formPerm]]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑[Finset.card (support (formPerm (attach l)))] = {length l}
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑(map (Finset.card ∘ support) [formPerm (attach l)]) = {length l}
simp only [map, Function.comp_apply]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑[length (attach l)] = {length l}

α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ∀ (x : { x // x ∈ l }), attach l ≠ [x]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑[Finset.card (support (formPerm (attach l)))] = {length l}
rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
no goals
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑[length (attach l)] = {length l}
simp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
x : { x // x ∈ l }
h : attach l = [x]
⊢ False
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ∀ (x : { x // x ∈ l }), attach l ≠ [x]
intro x h
no goals
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
x : { x // x ∈ l }
h : attach l = [x]
⊢ False
simp [h, Nat.succ_le_succ_iff] at hn
no goals
case h0
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ prod [formPerm (attach l)] = formPerm (attach l)
simp
no goals
case h1
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ∀ (σ : Equiv.Perm { x // x ∈ l }), σ ∈ [formPerm (attach l)] → IsCycle σ
simpa using isCycle_formPerm hl hn
no goals
case h2
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ Pairwise Perm.Disjoint [formPerm (attach l)]
simp