[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ Perm.Disjoint (formPerm l) (formPerm l') ↔ Disjoint l l'
[PROOFSTEP]
rw [disjoint_iff_eq_or_eq, List.Disjoint]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x) → ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
[PROOFSTEP]
rintro h x hx hx'
[GOAL]
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ False
[PROOFSTEP]
specialize h x
[GOAL]
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
h : ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
⊢ False
[PROOFSTEP]
rw [formPerm_apply_mem_eq_self_iff _ hl _ hx, formPerm_apply_mem_eq_self_iff _ hl' _ hx'] at h
[GOAL]
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
h : length l ≤ 1 ∨ length l' ≤ 1
⊢ False
[PROOFSTEP]
rcases h with (hl | hl')
[GOAL]
case mp.inl
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl✝ : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
hl : length l ≤ 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case mp.inr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl'✝ : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
hl' : length l' ≤ 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False) → ∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
intro h x
[GOAL]
case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
by_cases hx : x ∈ l
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
by_cases hx' : x ∈ l'
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
exact (h hx hx').elim
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : ¬x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
all_goals have := formPerm_eq_self_of_not_mem _ _ ‹_›; tauto
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : ¬x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
have := formPerm_eq_self_of_not_mem _ _ ‹_›
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : ¬x ∈ l'
this : ↑(formPerm l') x = x
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
tauto
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
have := formPerm_eq_self_of_not_mem _ _ ‹_›
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
this : ↑(formPerm l) x = x
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length l
⊢ IsCycle (formPerm l)
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl : Nodup []
hn : 2 ≤ length []
⊢ IsCycle (formPerm [])
[PROOFSTEP]
norm_num at hn
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x : α
l : List α
hl : Nodup (x :: l)
hn : 2 ≤ length (x :: l)
⊢ IsCycle (formPerm (x :: l))
[PROOFSTEP]
induction' l with y l generalizing x
[GOAL]
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l : List α
hl✝ : Nodup (x✝ :: l)
hn✝ : 2 ≤ length (x✝ :: l)
x : α
hl : Nodup [x]
hn : 2 ≤ length [x]
⊢ IsCycle (formPerm [x])
[PROOFSTEP]
norm_num at hn
[GOAL]
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ IsCycle (formPerm (x :: y :: l))
[PROOFSTEP]
use x
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ↑(formPerm (x :: y :: l)) y_1 ≠ y_1 → SameCycle (formPerm (x :: y :: l)) x y_1
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) x ≠ x
[PROOFSTEP]
rwa [formPerm_apply_mem_ne_self_iff _ hl _ (mem_cons_self _ _)]
[GOAL]
case h.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
⊢ ∀ ⦃y_1 : α⦄, ↑(formPerm (x :: y :: l)) y_1 ≠ y_1 → SameCycle (formPerm (x :: y :: l)) x y_1
[PROOFSTEP]
intro w hw
[GOAL]
case h.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
w : α
hw : ↑(formPerm (x :: y :: l)) w ≠ w
⊢ SameCycle (formPerm (x :: y :: l)) x w
[PROOFSTEP]
have : w ∈ x :: y :: l := mem_of_formPerm_ne_self _ _ hw
[GOAL]
case h.right
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
w : α
hw : ↑(formPerm (x :: y :: l)) w ≠ w
this : w ∈ x :: y :: l
⊢ SameCycle (formPerm (x :: y :: l)) x w
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem this
[GOAL]
case h.right.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
k : ℕ
hk : k < length (x :: y :: l)
hw : ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) k hk) ≠ nthLe (x :: y :: l) k hk
this : nthLe (x :: y :: l) k hk ∈ x :: y :: l
⊢ SameCycle (formPerm (x :: y :: l)) x (nthLe (x :: y :: l) k hk)
[PROOFSTEP]
use k
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l' : List α
x✝ : α
l✝ : List α
hl✝ : Nodup (x✝ :: l✝)
hn✝ : 2 ≤ length (x✝ :: l✝)
y : α
l : List α
tail_ih✝ : ∀ (x : α), Nodup (x :: l) → 2 ≤ length (x :: l) → IsCycle (formPerm (x :: l))
x : α
hl : Nodup (x :: y :: l)
hn : 2 ≤ length (x :: y :: l)
k : ℕ
hk : k < length (x :: y :: l)
hw : ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) k hk) ≠ nthLe (x :: y :: l) k hk
this : nthLe (x :: y :: l) k hk ∈ x :: y :: l
⊢ ↑(formPerm (x :: y :: l) ^ ↑k) x = nthLe (x :: y :: l) k hk
[PROOFSTEP]
simp only [zpow_ofNat, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length l
x : { x // x ∈ l }
⊢ 2 ≤ length (attach l)
[PROOFSTEP]
rwa [← length_attach] at hn
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn✝ : 2 ≤ length l
x : { x // x ∈ l }
hn : 2 ≤ length (attach l)
⊢ Nodup (attach l)
[PROOFSTEP]
rwa [← nodup_attach] at hl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length l
⊢ cycleType (formPerm (attach l)) = {length l}
[PROOFSTEP]
rw [← length_attach] at hn
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hn : 2 ≤ length (attach l)
⊢ cycleType (formPerm (attach l)) = {length l}
[PROOFSTEP]
rw [← nodup_attach] at hl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ cycleType (formPerm (attach l)) = {length l}
[PROOFSTEP]
rw [cycleType_eq [l.attach.formPerm]]
[GOAL]
α : 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}
[PROOFSTEP]
simp only [map, Function.comp_apply]
[GOAL]
α : 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}
[PROOFSTEP]
rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ↑[length (attach l)] = {length l}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup (attach l)
hn : 2 ≤ length (attach l)
⊢ ∀ (x : { x // x ∈ l }), attach l ≠ [x]
[PROOFSTEP]
intro x h
[GOAL]
α : 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
[PROOFSTEP]
simp [h, Nat.succ_le_succ_iff] at hn
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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 σ
[PROOFSTEP]
simpa using isCycle_formPerm hl hn
[GOAL]
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)]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = next l x hx
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l) (nthLe l k hk) = next l (nthLe l k hk) hx
[PROOFSTEP]
rw [next_nthLe _ hl, formPerm_apply_nthLe _ hl]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ HEq (fun x => List.formPerm l₁) fun x => List.formPerm l₂
[PROOFSTEP]
apply Function.hfunext
[GOAL]
case hα
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ Nodup (Quotient.mk (IsRotated.setoid α) l₁) = Nodup (Quotient.mk (IsRotated.setoid α) l₂)
case h
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ ∀ (a : Nodup (Quotient.mk (IsRotated.setoid α) l₁)) (a' : Nodup (Quotient.mk (IsRotated.setoid α) l₂)),
    HEq a a' → HEq (List.formPerm l₁) (List.formPerm l₂)
[PROOFSTEP]
ext
[GOAL]
case hα.a
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ Nodup (Quotient.mk (IsRotated.setoid α) l₁) ↔ Nodup (Quotient.mk (IsRotated.setoid α) l₂)
[PROOFSTEP]
exact h.nodup_iff
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ ∀ (a : Nodup (Quotient.mk (IsRotated.setoid α) l₁)) (a' : Nodup (Quotient.mk (IsRotated.setoid α) l₂)),
    HEq a a' → HEq (List.formPerm l₁) (List.formPerm l₂)
[PROOFSTEP]
intro h₁ h₂ _
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
h₁ : Nodup (Quotient.mk (IsRotated.setoid α) l₁)
h₂ : Nodup (Quotient.mk (IsRotated.setoid α) l₂)
a✝ : HEq h₁ h₂
⊢ HEq (List.formPerm l₁) (List.formPerm l₂)
[PROOFSTEP]
exact heq_of_eq (formPerm_eq_of_isRotated h₁ h)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Subsingleton s
⊢ formPerm s (_ : Nodup s) = 1
[PROOFSTEP]
induction' s using Quot.inductionOn with s
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : Subsingleton (Quot.mk Setoid.r s)
⊢ formPerm (Quot.mk Setoid.r s) (_ : Nodup (Quot.mk Setoid.r s)) = 1
[PROOFSTEP]
simp only [formPerm_coe, mk_eq_coe]
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : Subsingleton (Quot.mk Setoid.r s)
⊢ List.formPerm s = 1
[PROOFSTEP]
simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s✝¹ s' s✝ : Cycle α
h✝ : Subsingleton s✝
s : List α
h : List.length s ≤ 1
⊢ List.formPerm s = 1
[PROOFSTEP]
cases' s with hd tl
[GOAL]
case h.nil
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
h : List.length [] ≤ 1
⊢ List.formPerm [] = 1
[PROOFSTEP]
simp
[GOAL]
case h.cons
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : List.length (hd :: tl) ≤ 1
⊢ List.formPerm (hd :: tl) = 1
[PROOFSTEP]
simp only [length_eq_zero, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h
[GOAL]
case h.cons
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : tl = []
⊢ List.formPerm (hd :: tl) = 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
hn : Nontrivial s
⊢ IsCycle (formPerm s h)
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hn : Nontrivial (Quot.mk Setoid.r a✝)
⊢ IsCycle (formPerm (Quot.mk Setoid.r a✝) h)
[PROOFSTEP]
exact List.isCycle_formPerm h (length_nontrivial hn)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ s' : Cycle α
inst✝ : Fintype α
s : Cycle α
h : Nodup s
hn : Nontrivial s
⊢ support (formPerm s h) = toFinset s
[PROOFSTEP]
induction' s using Quot.inductionOn with s
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝¹ s' : Cycle α
inst✝ : Fintype α
s✝ : Cycle α
h✝ : Nodup s✝
hn✝ : Nontrivial s✝
s : List α
h : Nodup (Quot.mk Setoid.r s)
hn : Nontrivial (Quot.mk Setoid.r s)
⊢ support (formPerm (Quot.mk Setoid.r s) h) = toFinset (Quot.mk Setoid.r s)
[PROOFSTEP]
refine' support_formPerm_of_nodup s h _
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝¹ s' : Cycle α
inst✝ : Fintype α
s✝ : Cycle α
h✝ : Nodup s✝
hn✝ : Nontrivial s✝
s : List α
h : Nodup (Quot.mk Setoid.r s)
hn : Nontrivial (Quot.mk Setoid.r s)
⊢ ∀ (x : α), s ≠ [x]
[PROOFSTEP]
rintro _ rfl
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
s✝ s' : Cycle α
inst✝ : Fintype α
s : Cycle α
h✝ : Nodup s
hn✝ : Nontrivial s
x✝ : α
h : Nodup (Quot.mk Setoid.r [x✝])
hn : Nontrivial (Quot.mk Setoid.r [x✝])
⊢ False
[PROOFSTEP]
simpa [Nat.succ_le_succ_iff] using length_nontrivial hn
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
x : α
hx : ¬x ∈ s
⊢ ↑(formPerm s h) x = x
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
x : α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hx : ¬x ∈ Quot.mk Setoid.r a✝
⊢ ↑(formPerm (Quot.mk Setoid.r a✝) h) x = x
[PROOFSTEP]
simpa using List.formPerm_eq_self_of_not_mem _ _ hx
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
x : α
hx : x ∈ s
⊢ ↑(formPerm s h) x = next s h x hx
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
x : α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ ↑(formPerm (Quot.mk Setoid.r a✝) h) x = next (Quot.mk Setoid.r a✝) h x hx
[PROOFSTEP]
simpa using List.formPerm_apply_mem_eq_next h _ (by simp_all)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
x : α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ x ∈ a✝
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
⊢ formPerm (reverse s) (_ : Nodup (reverse s)) = (formPerm s h)⁻¹
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
⊢ formPerm (reverse (Quot.mk Setoid.r a✝)) (_ : Nodup (reverse (Quot.mk Setoid.r a✝))) =
    (formPerm (Quot.mk Setoid.r a✝) h)⁻¹
[PROOFSTEP]
simpa using formPerm_reverse _ h
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
hs : Nodup s
hs' : Nodup s'
⊢ formPerm s hs = formPerm s' hs' ↔ s = s' ∨ Subsingleton s ∧ Subsingleton s'
[PROOFSTEP]
rw [Cycle.length_subsingleton_iff, Cycle.length_subsingleton_iff]
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
hs : Nodup s
hs' : Nodup s'
⊢ formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
[PROOFSTEP]
revert s s'
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s s' : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ ∀ {s s' : Cycle α} {hs : Nodup s} {hs' : Nodup s'},
    formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
[PROOFSTEP]
intro s s'
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ {hs : Nodup s} {hs' : Nodup s'}, formPerm s hs = formPerm s' hs' ↔ s = s' ∨ length s ≤ 1 ∧ length s' ≤ 1
[PROOFSTEP]
apply @Quotient.inductionOn₂' _ _ _ _ _ s s'
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
    formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
      Quotient.mk'' a₁ = Quotient.mk'' a₂ ∨ length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1
[PROOFSTEP]
intro l l'
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
⊢ ∀ {hs : Nodup (Quotient.mk'' l)} {hs' : Nodup (Quotient.mk'' l')},
    formPerm (Quotient.mk'' l) hs = formPerm (Quotient.mk'' l') hs' ↔
      Quotient.mk'' l = Quotient.mk'' l' ∨ length (Quotient.mk'' l) ≤ 1 ∧ length (Quotient.mk'' l') ≤ 1
[PROOFSTEP]
simp_all
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
⊢ ∀ {hs : List.Nodup l} {hs' : List.Nodup l'},
    List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
[PROOFSTEP]
intro hs hs'
[GOAL]
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
⊢ List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
⊢ List.formPerm l = List.formPerm l' → l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
⊢ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1 → List.formPerm l = List.formPerm l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
h : List.formPerm l = List.formPerm l'
⊢ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
[PROOFSTEP]
simp_all only [formPerm_eq_formPerm_iff]
[GOAL]
case mpr
α✝ : Type u_1
inst✝¹ : DecidableEq α✝
s✝ s'✝ : Cycle α✝
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hs : List.Nodup l
hs' : List.Nodup l'
h : l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1
⊢ List.formPerm l = List.formPerm l'
[PROOFSTEP]
simp_all only [formPerm_eq_formPerm_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ toList 1 x = []
[PROOFSTEP]
simp [toList, cycleOf_one]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
⊢ toList p x = [] ↔ ¬x ∈ support p
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ length (toList p x) = Finset.card (support (cycleOf p x))
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ toList p x ≠ [y]
[PROOFSTEP]
intro H
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
H : toList p x = [y]
⊢ False
[PROOFSTEP]
simpa [card_support_ne_one] using congr_arg length H
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
⊢ 2 ≤ length (toList p x) ↔ x ∈ support p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hn : n < length (toList p x)
⊢ nthLe (toList p x) n hn = ↑(p ^ n) x
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
h : x ∈ support p
⊢ nthLe (toList p x) 0 (_ : 0 < length (toList p x)) = x
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ y ∈ toList p x ↔ SameCycle p x y ∧ x ∈ support p
[PROOFSTEP]
simp only [toList, mem_range, mem_map]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y) ↔ SameCycle p x y ∧ x ∈ support p
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y) → SameCycle p x y ∧ x ∈ support p
[PROOFSTEP]
rintro ⟨n, hx, rfl⟩
[GOAL]
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < Finset.card (support (cycleOf p x))
⊢ SameCycle p x (↑(p ^ n) x) ∧ x ∈ support p
[PROOFSTEP]
refine' ⟨⟨n, rfl⟩, _⟩
[GOAL]
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < Finset.card (support (cycleOf p x))
⊢ x ∈ support p
[PROOFSTEP]
contrapose! hx
[GOAL]
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : ¬x ∈ support p
⊢ Finset.card (support (cycleOf p x)) ≤ n
[PROOFSTEP]
rw [← support_cycleOf_eq_nil_iff] at hx
[GOAL]
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : support (cycleOf p x) = ∅
⊢ Finset.card (support (cycleOf p x)) ≤ n
[PROOFSTEP]
simp [hx]
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ SameCycle p x y ∧ x ∈ support p → ∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y
[PROOFSTEP]
rintro ⟨h, hx⟩
[GOAL]
case mpr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
h : SameCycle p x y
hx : x ∈ support p
⊢ ∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y
[PROOFSTEP]
simpa using h.exists_pow_eq_of_mem_support hx
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
⊢ Nodup (toList p x)
[PROOFSTEP]
by_cases hx : p x = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ↑p x = x
⊢ Nodup (toList p x)
[PROOFSTEP]
rw [← not_mem_support, ← toList_eq_nil_iff] at hx
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝ : ↑p x = x
hx : toList p x = []
⊢ Nodup (toList p x)
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
⊢ Nodup (toList p x)
[PROOFSTEP]
have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
⊢ Nodup (toList p x)
[PROOFSTEP]
rw [nodup_iff_nthLe_inj]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
⊢ ∀ (i j : ℕ) (h₁ : i < length (toList p x)) (h₂ : j < length (toList p x)),
    nthLe (toList p x) i h₁ = nthLe (toList p x) j h₂ → i = j
[PROOFSTEP]
rintro n m hn hm
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
n m : ℕ
hn : n < length (toList p x)
hm : m < length (toList p x)
⊢ nthLe (toList p x) n hn = nthLe (toList p x) m hm → n = m
[PROOFSTEP]
rw [length_toList, ← hc.orderOf] at hm hn
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx : ¬↑p x = x
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ nthLe (toList p x) n hn✝ = nthLe (toList p x) m hm✝ → n = m
[PROOFSTEP]
rw [← cycleOf_apply_self, ← Ne.def, ← mem_support] at hx
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ nthLe (toList p x) n hn✝ = nthLe (toList p x) m hm✝ → n = m
[PROOFSTEP]
rw [nthLe_toList, nthLe_toList, ← cycleOf_pow_apply_self p x n, ← cycleOf_pow_apply_self p x m]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n m : ℕ
hn✝ : n < length (toList p x)
hn : n < orderOf (cycleOf p x)
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ n) x = ↑(cycleOf p x ^ m) x → n = m
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
m : ℕ
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ m) x → Nat.zero = m
[PROOFSTEP]
cases' m with m
[GOAL]
case neg.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
m : ℕ
hm✝ : m < length (toList p x)
hm : m < orderOf (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ m) x → Nat.succ n = m
[PROOFSTEP]
cases' m with m
[GOAL]
case neg.zero.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.zero = Nat.zero
[PROOFSTEP]
simp
[GOAL]
case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.zero = Nat.succ m
[PROOFSTEP]
rw [← hc.support_pow_of_pos_of_lt_orderOf m.zero_lt_succ hm, mem_support, cycleOf_pow_apply_self] at hx
[GOAL]
case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hc : IsCycle (cycleOf p x)
hn✝ : Nat.zero < length (toList p x)
hn : Nat.zero < orderOf (cycleOf p x)
m : ℕ
hx : ↑(p ^ Nat.succ m) x ≠ x
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.zero) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.zero = Nat.succ m
[PROOFSTEP]
simp [hx.symm]
[GOAL]
case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.succ n = Nat.zero
[PROOFSTEP]
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support, cycleOf_pow_apply_self] at hx
[GOAL]
case neg.succ.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hc : IsCycle (cycleOf p x)
n : ℕ
hx : ↑(p ^ Nat.succ n) x ≠ x
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
hm✝ : Nat.zero < length (toList p x)
hm : Nat.zero < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.zero) x → Nat.succ n = Nat.zero
[PROOFSTEP]
simp [hx]
[GOAL]
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x → Nat.succ n = Nat.succ m
[PROOFSTEP]
intro h
[GOAL]
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
⊢ Nat.succ n = Nat.succ m
[PROOFSTEP]
have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ := Nat.not_dvd_of_pos_of_lt n.zero_lt_succ hn
[GOAL]
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : ¬orderOf (cycleOf p x) ∣ Nat.succ n
⊢ Nat.succ n = Nat.succ m
[PROOFSTEP]
have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm
[GOAL]
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : ¬orderOf (cycleOf p x) ∣ Nat.succ n
hm' : ¬orderOf (cycleOf p x) ∣ Nat.succ m
⊢ Nat.succ n = Nat.succ m
[PROOFSTEP]
rw [← hc.support_pow_eq_iff] at hn' hm'
[GOAL]
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ Nat.succ n = Nat.succ m
[PROOFSTEP]
rw [← Nat.mod_eq_of_lt hn, ← Nat.mod_eq_of_lt hm, ← pow_inj_mod]
[GOAL]
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ cycleOf p x ^ Nat.succ n = cycleOf p x ^ Nat.succ m
[PROOFSTEP]
refine' support_congr _ _
[GOAL]
case neg.succ.succ.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ support (cycleOf p x ^ Nat.succ n) ⊆ support (cycleOf p x ^ Nat.succ m)
[PROOFSTEP]
rw [hm', hn']
[GOAL]
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ ∀ (x_1 : α),
    x_1 ∈ support (cycleOf p x ^ Nat.succ m) → ↑(cycleOf p x ^ Nat.succ n) x_1 = ↑(cycleOf p x ^ Nat.succ m) x_1
[PROOFSTEP]
rw [hm']
[GOAL]
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
⊢ ∀ (x_1 : α), x_1 ∈ support (cycleOf p x) → ↑(cycleOf p x ^ Nat.succ n) x_1 = ↑(cycleOf p x ^ Nat.succ m) x_1
[PROOFSTEP]
intro y hy
[GOAL]
case neg.succ.succ.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
y : α
hy : y ∈ support (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) y = ↑(cycleOf p x ^ Nat.succ m) y
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)
[GOAL]
case neg.succ.succ.refine'_2.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
hx✝¹ : ¬↑p x = x
hx✝ : ↑(cycleOf p x) x ≠ x
hx : x ∈ support (cycleOf p x)
hc : IsCycle (cycleOf p x)
n : ℕ
hn✝ : Nat.succ n < length (toList p x)
hn : Nat.succ n < orderOf (cycleOf p x)
m : ℕ
hm✝ : Nat.succ m < length (toList p x)
hm : Nat.succ m < orderOf (cycleOf p x)
h : ↑(cycleOf p x ^ Nat.succ n) x = ↑(cycleOf p x ^ Nat.succ m) x
hn' : support (cycleOf p x ^ Nat.succ n) = support (cycleOf p x)
hm' : support (cycleOf p x ^ Nat.succ m) = support (cycleOf p x)
k : ℕ
hy : ↑(cycleOf p x ^ k) x ∈ support (cycleOf p x)
⊢ ↑(cycleOf p x ^ Nat.succ n) (↑(cycleOf p x ^ k) x) = ↑(cycleOf p x ^ Nat.succ m) (↑(cycleOf p x ^ k) x)
[PROOFSTEP]
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
  (Commute.pow_pow_self _ _ _).eq]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy : y ∈ toList p x
⊢ next (toList p x) y hy = ↑p y
[PROOFSTEP]
rw [mem_toList_iff] at hy
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
⊢ next (toList p x) y hy✝ = ↑p y
[PROOFSTEP]
obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk' : ↑(p ^ k) x = y
⊢ next (toList p x) y hy✝ = ↑p y
[PROOFSTEP]
rw [← nthLe_toList p x k (by simpa using hk)] at hk'
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk' : ↑(p ^ k) x = y
⊢ k < length (toList p x)
[PROOFSTEP]
simpa using hk
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ next (toList p x) y hy✝ = ↑p y
[PROOFSTEP]
simp_rw [← hk']
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ next (toList p x) (nthLe (toList p x) k (_ : k < length (toList p x)))
      (_ : nthLe (toList p x) k (_ : k < length (toList p x)) ∈ toList p x) =
    ↑p (nthLe (toList p x) k (_ : k < length (toList p x)))
[PROOFSTEP]
rw [next_nthLe _ (nodup_toList _ _), nthLe_toList, nthLe_toList, ← mul_apply, ← pow_succ, length_toList,
  pow_apply_eq_pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ IsCycle (cycleOf p x)
[PROOFSTEP]
exact isCycle_cycleOf _ (mem_support.mp hy.right)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ toList p (↑(p ^ k) x) = rotate (toList p x) k
[PROOFSTEP]
apply ext_nthLe
[GOAL]
case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ length (toList p (↑(p ^ k) x)) = length (rotate (toList p x) k)
[PROOFSTEP]
simp only [length_toList, cycleOf_self_apply_pow, length_rotate]
[GOAL]
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ ∀ (n : ℕ) (h₁ : n < length (toList p (↑(p ^ k) x))) (h₂ : n < length (rotate (toList p x) k)),
    nthLe (toList p (↑(p ^ k) x)) n h₁ = nthLe (rotate (toList p x) k) n h₂
[PROOFSTEP]
intro n hn hn'
[GOAL]
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k n : ℕ
hn : n < length (toList p (↑(p ^ k) x))
hn' : n < length (rotate (toList p x) k)
⊢ nthLe (toList p (↑(p ^ k) x)) n hn = nthLe (rotate (toList p x) k) n hn'
[PROOFSTEP]
rw [nthLe_toList, nthLe_rotate, nthLe_toList, length_toList, pow_mod_card_support_cycleOf_self_apply, pow_add,
  mul_apply]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
⊢ toList f x ~r toList f y
[PROOFSTEP]
by_cases hx : x ∈ f.support
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : x ∈ support f
⊢ toList f x ~r toList f y
[PROOFSTEP]
obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx
[GOAL]
case pos.intro.zero.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : x ∈ support f
w✝ : Nat.zero < Finset.card (support (cycleOf f x))
hy : ↑(f ^ Nat.zero) x = y
⊢ toList f x ~r toList f y
[PROOFSTEP]
simp only [coe_one, id.def, pow_zero, Nat.zero_eq] at hy
[GOAL]
case pos.intro.zero.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : x ∈ support f
w✝ : Nat.zero < Finset.card (support (cycleOf f x))
hy : x = y
⊢ toList f x ~r toList f y
[PROOFSTEP]
simp [hy, IsRotated.refl]
[GOAL]
case pos.intro.succ.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
w✝ : Nat.succ k < Finset.card (support (cycleOf f x))
hy : ↑(f ^ Nat.succ k) x = y
⊢ toList f x ~r toList f y
[PROOFSTEP]
use k.succ
[GOAL]
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : x ∈ support f
k : ℕ
w✝ : Nat.succ k < Finset.card (support (cycleOf f x))
hy : ↑(f ^ Nat.succ k) x = y
⊢ rotate (toList f x) (Nat.succ k) = toList f y
[PROOFSTEP]
rw [← toList_pow_apply_eq_rotate, hy]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ toList f x ~r toList f y
[PROOFSTEP]
rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x y : α
h : SameCycle f x y
hx : ¬x ∈ support f
⊢ ¬y ∈ support f
[PROOFSTEP]
rwa [← h.mem_support_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ ↑(p ^ n) x ∈ toList p x ↔ x ∈ support p
[PROOFSTEP]
rw [mem_toList_iff, and_iff_right_iff_imp]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ x ∈ support p → SameCycle p x (↑(p ^ n) x)
[PROOFSTEP]
refine' fun _ => SameCycle.symm _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
x✝ : x ∈ support p
⊢ SameCycle p (↑(p ^ n) x) x
[PROOFSTEP]
rw [sameCycle_pow_left]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ x : α
⊢ toList (formPerm []) x = []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ x y : α
⊢ toList (formPerm [x]) y = []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
[PROOFSTEP]
have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
[PROOFSTEP]
have hs : l.formPerm.support = l.toFinset :=
  by
  refine' support_formPerm_of_nodup _ hn _
  rintro _ rfl
  simp [Nat.succ_le_succ_iff] at hl
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ support (formPerm l) = toFinset l
[PROOFSTEP]
refine' support_formPerm_of_nodup _ hn _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ ∀ (x : α), l ≠ [x]
[PROOFSTEP]
rintro _ rfl
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x x✝ : α
hl : 2 ≤ length [x✝]
hn : Nodup [x✝]
hc : IsCycle (formPerm [x✝])
⊢ False
[PROOFSTEP]
simp [Nat.succ_le_succ_iff] at hl
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
[PROOFSTEP]
rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)) = l
[PROOFSTEP]
refine' ext_get (by simp) fun k hk hk' => _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l))) = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
k : ℕ
hk : k < length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
hk' : k < length l
⊢ List.get (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
      { val := k, isLt := hk } =
    List.get l { val := k, isLt := hk' }
[PROOFSTEP]
simp [formPerm_pow_apply_nthLe _ hn, Nat.mod_eq_of_lt hk']
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
k : ℕ
hk : k < length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
hk' : k < length l
⊢ nthLe l k (_ : k < length l) = List.get l { val := k, isLt := hk' }
[PROOFSTEP]
rw [nthLe_eq]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ nthLe l 0 (_ : 0 < length l) ∈ support (formPerm l)
[PROOFSTEP]
simpa [hs] using get_mem _ _ _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
x : α
hx : x ∈ l
⊢ toList (formPerm l) x ~r l
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := get_of_mem hx
[GOAL]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
⊢ toList (formPerm l) (List.get l k) ~r l
[PROOFSTEP]
have hr : l ~r l.rotate k := ⟨k, rfl⟩
[GOAL]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm l) (List.get l k) ~r l
[PROOFSTEP]
rw [formPerm_eq_of_isRotated hn hr]
[GOAL]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k)) (List.get l k) ~r l
[PROOFSTEP]
rw [get_eq_get_rotate l k k]
[GOAL]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k))
      (List.get (rotate l ↑k)
        { val := (length l - ↑k % length l + ↑k) % length l,
          isLt := (_ : (length l - ↑k % length l + ↑k) % length l < length (rotate l ↑k)) }) ~r
    l
[PROOFSTEP]
simp only [Nat.mod_eq_of_lt k.2, tsub_add_cancel_of_le (le_of_lt k.2), Nat.mod_self]
[GOAL]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k)) (List.get (rotate l ↑k) { val := 0, isLt := (_ : 0 < length (rotate l ↑k)) }) ~r l
[PROOFSTEP]
erw [toList_formPerm_nontrivial]
[GOAL]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ rotate l ↑k ~r l
[PROOFSTEP]
simp
[GOAL]
case intro.refl.hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ 2 ≤ length (rotate l ↑k)
[PROOFSTEP]
simpa using hl
[GOAL]
case intro.refl.hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ Nodup (rotate l ↑k)
[PROOFSTEP]
simpa using hn
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
⊢ formPerm (toList f x) = cycleOf f x
[PROOFSTEP]
by_cases hx : f x = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ↑f x = x
⊢ formPerm (toList f x) = cycleOf f x
[PROOFSTEP]
rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (not_mem_support.mpr hx), formPerm_nil]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ formPerm (toList f x) = cycleOf f x
[PROOFSTEP]
ext y
[GOAL]
case neg.H
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
y : α
⊢ ↑(formPerm (toList f x)) y = ↑(cycleOf f x) y
[PROOFSTEP]
by_cases hy : SameCycle f x y
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
y : α
hy : SameCycle f x y
⊢ ↑(formPerm (toList f x)) y = ↑(cycleOf f x) y
[PROOFSTEP]
obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
k : ℕ
w✝ : k < Finset.card (support (cycleOf f x))
hy : SameCycle f x (↑(f ^ k) x)
⊢ ↑(formPerm (toList f x)) (↑(f ^ k) x) = ↑(cycleOf f x) (↑(f ^ k) x)
[PROOFSTEP]
rw [cycleOf_apply_apply_pow_self, List.formPerm_apply_mem_eq_next (nodup_toList f x), next_toList_eq_apply, pow_succ,
  mul_apply]
[GOAL]
case pos.intro.intro.hy
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
k : ℕ
w✝ : k < Finset.card (support (cycleOf f x))
hy : SameCycle f x (↑(f ^ k) x)
⊢ ↑(f ^ k) x ∈ toList f x
[PROOFSTEP]
rw [mem_toList_iff]
[GOAL]
case pos.intro.intro.hy
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
k : ℕ
w✝ : k < Finset.card (support (cycleOf f x))
hy : SameCycle f x (↑(f ^ k) x)
⊢ SameCycle f x (↑(f ^ k) x) ∧ x ∈ support f
[PROOFSTEP]
exact ⟨⟨k, rfl⟩, mem_support.mpr hx⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
y : α
hy : ¬SameCycle f x y
⊢ ↑(formPerm (toList f x)) y = ↑(cycleOf f x) y
[PROOFSTEP]
rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_not_mem]
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
hx : ¬↑f x = x
y : α
hy : ¬SameCycle f x y
⊢ ¬y ∈ toList f x
[PROOFSTEP]
simp [mem_toList_iff, hy]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : IsCycle f
⊢ ∀ (a a' : α),
    Multiset α →
      ∀ (b : Cycle α),
        HEq (if ↑f a = a then if ↑f a' = a' then b else ↑(toList f a') else ↑(toList f a))
          (if ↑f a' = a' then if ↑f a = a then b else ↑(toList f a) else ↑(toList f a'))
[PROOFSTEP]
intro x y _ s
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
⊢ HEq (if ↑f x = x then if ↑f y = y then s else ↑(toList f y) else ↑(toList f x))
    (if ↑f y = y then if ↑f x = x then s else ↑(toList f x) else ↑(toList f y))
[PROOFSTEP]
refine' heq_of_eq _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
⊢ (if ↑f x = x then if ↑f y = y then s else ↑(toList f y) else ↑(toList f x)) =
    if ↑f y = y then if ↑f x = x then s else ↑(toList f x) else ↑(toList f y)
[PROOFSTEP]
split_ifs with hx hy hy
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ↑f x = x
hy : ↑f y = y
⊢ s = s
[PROOFSTEP]
try rfl
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ↑f x = x
hy : ↑f y = y
⊢ s = s
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ↑f x = x
hy : ¬↑f y = y
⊢ ↑(toList f y) = ↑(toList f y)
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ↑f x = x
hy : ¬↑f y = y
⊢ ↑(toList f y) = ↑(toList f y)
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬↑f x = x
hy : ↑f y = y
⊢ ↑(toList f x) = ↑(toList f x)
[PROOFSTEP]
try rfl
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬↑f x = x
hy : ↑f y = y
⊢ ↑(toList f x) = ↑(toList f x)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬↑f x = x
hy : ¬↑f y = y
⊢ ↑(toList f x) = ↑(toList f y)
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬↑f x = x
hy : ¬↑f y = y
⊢ ↑(toList f x) = ↑(toList f y)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬↑f x = x
hy : ¬↑f y = y
⊢ ↑(toList f x) = ↑(toList f y)
[PROOFSTEP]
have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬↑f x = x
hy : ¬↑f y = y
hc : SameCycle f x y
⊢ ↑(toList f x) = ↑(toList f y)
[PROOFSTEP]
exact Quotient.sound' hc.toList_isRotated
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ toCycle f hf = ↑(toList f x)
[PROOFSTEP]
have key : (Finset.univ : Finset α).val = x ::ₘ Finset.univ.val.erase x := by simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
key : Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
⊢ toCycle f hf = ↑(toList f x)
[PROOFSTEP]
rw [toCycle, key]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
key : Finset.univ.val = x ::ₘ Multiset.erase Finset.univ.val x
⊢ Multiset.recOn (x ::ₘ Multiset.erase Finset.univ.val x) (Quot.mk Setoid.r [])
      (fun x x_1 l => if ↑f x = x then l else ↑(toList f x))
      (_ :
        ∀ (x y : α),
          Multiset α →
            ∀ (s : Cycle α),
              HEq (if ↑f x = x then if ↑f y = y then s else ↑(toList f y) else ↑(toList f x))
                (if ↑f y = y then if ↑f x = x then s else ↑(toList f x) else ↑(toList f y))) =
    ↑(toList f x)
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : IsCycle f
⊢ Cycle.Nodup (toCycle f hf)
[PROOFSTEP]
obtain ⟨x, hx, -⟩ := id hf
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ Cycle.Nodup (toCycle f hf)
[PROOFSTEP]
simpa [toCycle_eq_toList f hf x hx] using nodup_toList _ _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : IsCycle f
⊢ Cycle.Nontrivial (toCycle f hf)
[PROOFSTEP]
obtain ⟨x, hx, -⟩ := id hf
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ Cycle.Nontrivial (toCycle f hf)
[PROOFSTEP]
simp [toCycle_eq_toList f hf x hx, hx, Cycle.nontrivial_coe_nodup_iff (nodup_toList _ _)]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : { f // IsCycle f }
⊢ (fun s =>
        { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
          property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) })
      ((fun f =>
          { val := toCycle ↑f (_ : IsCycle ↑f),
            property :=
              (_ : Cycle.Nodup (toCycle ↑f (_ : IsCycle ↑f)) ∧ Cycle.Nontrivial (toCycle ↑f (_ : IsCycle ↑f))) })
        f) =
    f
[PROOFSTEP]
obtain ⟨x, hx, -⟩ := id f.prop
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : { f // IsCycle f }
x : α
hx : ↑↑f x ≠ x
⊢ (fun s =>
        { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
          property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) })
      ((fun f =>
          { val := toCycle ↑f (_ : IsCycle ↑f),
            property :=
              (_ : Cycle.Nodup (toCycle ↑f (_ : IsCycle ↑f)) ∧ Cycle.Nontrivial (toCycle ↑f (_ : IsCycle ↑f))) })
        f) =
    f
[PROOFSTEP]
simpa [toCycle_eq_toList (f : Perm α) f.prop x hx, formPerm_toList, Subtype.ext_iff] using f.prop.cycleOf_eq hx
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
s : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s }
⊢ (fun f =>
        { val := toCycle ↑f (_ : IsCycle ↑f),
          property :=
            (_ : Cycle.Nodup (toCycle ↑f (_ : IsCycle ↑f)) ∧ Cycle.Nontrivial (toCycle ↑f (_ : IsCycle ↑f))) })
      ((fun s =>
          { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
            property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) })
        s) =
    s
[PROOFSTEP]
rcases s with ⟨⟨s⟩, hn, ht⟩
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
val✝ : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
⊢ (fun f =>
        { val := toCycle ↑f (_ : IsCycle ↑f),
          property :=
            (_ : Cycle.Nodup (toCycle ↑f (_ : IsCycle ↑f)) ∧ Cycle.Nontrivial (toCycle ↑f (_ : IsCycle ↑f))) })
      ((fun s =>
          { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
            property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) })
        { val := Quot.mk Setoid.r s,
          property := (_ : Cycle.Nodup (Quot.mk Setoid.r s) ∧ Cycle.Nontrivial (Quot.mk Setoid.r s)) }) =
    { val := Quot.mk Setoid.r s,
      property := (_ : Cycle.Nodup (Quot.mk Setoid.r s) ∧ Cycle.Nontrivial (Quot.mk Setoid.r s)) }
[PROOFSTEP]
obtain ⟨x, -, -, hx, -⟩ := id ht
[GOAL]
case mk.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hx : x ∈ Quot.mk Setoid.r s
⊢ (fun f =>
        { val := toCycle ↑f (_ : IsCycle ↑f),
          property :=
            (_ : Cycle.Nodup (toCycle ↑f (_ : IsCycle ↑f)) ∧ Cycle.Nontrivial (toCycle ↑f (_ : IsCycle ↑f))) })
      ((fun s =>
          { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
            property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) })
        { val := Quot.mk Setoid.r s,
          property := (_ : Cycle.Nodup (Quot.mk Setoid.r s) ∧ Cycle.Nontrivial (Quot.mk Setoid.r s)) }) =
    { val := Quot.mk Setoid.r s,
      property := (_ : Cycle.Nodup (Quot.mk Setoid.r s) ∧ Cycle.Nontrivial (Quot.mk Setoid.r s)) }
[PROOFSTEP]
have hl : 2 ≤ s.length := by simpa using Cycle.length_nontrivial ht
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hx : x ∈ Quot.mk Setoid.r s
⊢ 2 ≤ length s
[PROOFSTEP]
simpa using Cycle.length_nontrivial ht
[GOAL]
case mk.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hx : x ∈ Quot.mk Setoid.r s
hl : 2 ≤ length s
⊢ (fun f =>
        { val := toCycle ↑f (_ : IsCycle ↑f),
          property :=
            (_ : Cycle.Nodup (toCycle ↑f (_ : IsCycle ↑f)) ∧ Cycle.Nontrivial (toCycle ↑f (_ : IsCycle ↑f))) })
      ((fun s =>
          { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
            property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) })
        { val := Quot.mk Setoid.r s,
          property := (_ : Cycle.Nodup (Quot.mk Setoid.r s) ∧ Cycle.Nontrivial (Quot.mk Setoid.r s)) }) =
    { val := Quot.mk Setoid.r s,
      property := (_ : Cycle.Nodup (Quot.mk Setoid.r s) ∧ Cycle.Nontrivial (Quot.mk Setoid.r s)) }
[PROOFSTEP]
simp only [Cycle.mk_eq_coe, Cycle.nodup_coe_iff, Cycle.mem_coe_iff, Subtype.coe_mk, Cycle.formPerm_coe] at hn hx ⊢
[GOAL]
case mk.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ { val := toCycle (formPerm s) (_ : IsCycle (formPerm s)),
      property :=
        (_ : (fun s => Cycle.Nodup s ∧ Cycle.Nontrivial s) (toCycle (formPerm s) (_ : IsCycle (formPerm s)))) } =
    { val := ↑s, property := (_ : (fun s => Cycle.Nodup s ∧ Cycle.Nontrivial s) ↑s) }
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ ↑{ val := toCycle (formPerm s) (_ : IsCycle (formPerm s)),
        property :=
          (_ : (fun s => Cycle.Nodup s ∧ Cycle.Nontrivial s) (toCycle (formPerm s) (_ : IsCycle (formPerm s)))) } =
    ↑{ val := ↑s, property := (_ : (fun s => Cycle.Nodup s ∧ Cycle.Nontrivial s) ↑s) }
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ toCycle (formPerm s)
      (_ : IsCycle ↑{ val := formPerm s, property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) }) =
    ↑s
[PROOFSTEP]
rw [toCycle_eq_toList _ _ x]
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ ↑(toList (formPerm s) x) = ↑s
[PROOFSTEP]
refine' Quotient.sound' _
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ Setoid.r (toList (formPerm s) x) s
[PROOFSTEP]
exact toList_formPerm_isRotated_self _ hl hn _ hx
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ ↑(formPerm s) x ≠ x
[PROOFSTEP]
rw [← mem_support, support_formPerm_of_nodup _ hn]
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ x ∈ toFinset s
[PROOFSTEP]
simpa using hx
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r s)
ht : Cycle.Nontrivial (Quot.mk Setoid.r s)
x : α
hl : 2 ≤ length s
hn : Nodup s
hx : x ∈ s
⊢ ∀ (x : α), s ≠ [x]
[PROOFSTEP]
rintro _ rfl
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝¹ : α
val✝ : Cycle α
x x✝ : α
hn✝ : Cycle.Nodup (Quot.mk Setoid.r [x✝])
ht : Cycle.Nontrivial (Quot.mk Setoid.r [x✝])
hl : 2 ≤ length [x✝]
hn : Nodup [x✝]
hx : x ∈ [x✝]
⊢ False
[PROOFSTEP]
simp [Nat.succ_le_succ_iff] at hl
[GOAL]
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
[PROOFSTEP]
obtain ⟨x, hx, hy⟩ := id hf
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
[PROOFSTEP]
refine' ⟨f.toList x, ⟨nodup_toList f x, _⟩, _⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ Cycle.formPerm ↑(toList f x) (_ : Nodup (toList f x)) = f
[PROOFSTEP]
simp [formPerm_toList, hf.cycleOf_eq hx]
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ∀ (y : Cycle α), (fun s => ∃ h, Cycle.formPerm s h = f) y → y = ↑(toList f x)
[PROOFSTEP]
rintro ⟨l⟩ ⟨hn, rfl⟩
[GOAL]
case intro.intro.intro.refine'_2.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ Quot.mk Setoid.r l = ↑(toList (Cycle.formPerm (Quot.mk Setoid.r l) hn) x)
[PROOFSTEP]
simp only [Cycle.mk_eq_coe, Cycle.coe_eq_coe, Subtype.coe_mk, Cycle.formPerm_coe]
[GOAL]
case intro.intro.intro.refine'_2.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ l ~r toList (formPerm l) x
[PROOFSTEP]
refine' (toList_formPerm_isRotated_self _ _ hn _ _).symm
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ 2 ≤ length l
[PROOFSTEP]
contrapose! hx
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x = x
[PROOFSTEP]
suffices formPerm l = 1 by simp [this]
[GOAL]
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
this : formPerm l = 1
⊢ ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x = x
[PROOFSTEP]
simp [this]
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ formPerm l = 1
[PROOFSTEP]
rw [formPerm_eq_one_iff _ hn]
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ length l ≤ 1
[PROOFSTEP]
exact Nat.le_of_lt_succ hx
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ l
[PROOFSTEP]
rw [← mem_toFinset]
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ toFinset l
[PROOFSTEP]
refine' support_formPerm_le l _
[GOAL]
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ support (formPerm l)
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
⊢ ∃! s, Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f
[PROOFSTEP]
obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
⊢ ∃! s_1, Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) = Cycle.formPerm s hs
[PROOFSTEP]
refine' ⟨⟨s, hs⟩, rfl, _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
⊢ ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 => Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) = Cycle.formPerm s hs) y → y = { val := s, property := hs }
[PROOFSTEP]
rintro ⟨t, ht⟩ ht'
[GOAL]
case intro.intro.intro.mk
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
t : Cycle α
ht : Cycle.Nodup t
ht' : Cycle.formPerm ↑{ val := t, property := ht } (_ : Cycle.Nodup ↑{ val := t, property := ht }) = Cycle.formPerm s hs
⊢ { val := t, property := ht } = { val := s, property := hs }
[PROOFSTEP]
simpa using hs' _ ⟨ht, ht'⟩
[GOAL]
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
⊢ ∃! s, Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f
[PROOFSTEP]
obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.existsUnique_cycle_subtype
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ∃! s, Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f
[PROOFSTEP]
refine' ⟨⟨s, hn, _⟩, _, _⟩
[GOAL]
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ Cycle.Nontrivial s
[PROOFSTEP]
rw [hn.nontrivial_iff]
[GOAL]
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ¬Cycle.Subsingleton s
[PROOFSTEP]
subst f
[GOAL]
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
⊢ ¬Cycle.Subsingleton s
[PROOFSTEP]
intro H
[GOAL]
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
H : Cycle.Subsingleton s
⊢ False
[PROOFSTEP]
refine' hf.ne_one _
[GOAL]
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
H : Cycle.Subsingleton s
⊢ Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = 1
[PROOFSTEP]
simpa using Cycle.formPerm_subsingleton _ H
[GOAL]
case intro.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f)
    { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
[PROOFSTEP]
simpa using hs
[GOAL]
case intro.mk.intro.refine'_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ∀ (y : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y →
      y = { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
[PROOFSTEP]
rintro ⟨t, ht, ht'⟩ ht''
[GOAL]
case intro.mk.intro.refine'_3.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
t : Cycle α
ht : Cycle.Nodup t
ht' : Cycle.Nontrivial t
ht'' :
  Cycle.formPerm ↑{ val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) }
      (_ : Cycle.Nodup ↑{ val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) }) =
    f
⊢ { val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) } =
    { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
[PROOFSTEP]
simpa using hs' ⟨t, ht⟩ ht''
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s } → { f // IsCycle f } :=
  fun s =>
    { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
      property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) }
⊢ Function.Bijective f
[PROOFSTEP]
rw [Function.bijective_iff_existsUnique]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s } → { f // IsCycle f } :=
  fun s =>
    { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
      property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) }
⊢ ∀ (b : { f // IsCycle f }), ∃! a, f a = b
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f✝ : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s } → { f // IsCycle f } :=
  fun s =>
    { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
      property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) }
f : Perm α
hf : IsCycle f
⊢ ∃! a, f✝ a = { val := f, property := hf }
[PROOFSTEP]
simp only [Subtype.ext_iff]
[GOAL]
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f✝ : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s } → { f // IsCycle f } :=
  fun s =>
    { val := Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s),
      property := (_ : IsCycle (Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s))) }
f : Perm α
hf : IsCycle f
⊢ ∃! a, Cycle.formPerm ↑a (_ : Cycle.Nodup ↑a) = f
[PROOFSTEP]
exact hf.existsUnique_cycle_nontrivial_subtype