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

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
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
x : α
⊢ formPerm (toList f x) = cycleOf f x
by_cases hx : f x = x
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
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
ext y
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

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
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
by_cases hy : SameCycle f x y
no goals
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
rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (not_mem_support.mpr hx),
  formPerm_nil]
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)
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
obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)
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
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)
rw [cycleOf_apply_apply_pow_self, List.formPerm_apply_mem_eq_next (nodup_toList f x),
  next_toList_eq_apply, pow_succ, mul_apply]
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
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
rw [mem_toList_iff]
no goals
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
exact ⟨⟨k, rfl⟩, mem_support.mpr hx⟩
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
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
rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_not_mem]
no goals
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
simp [mem_toList_iff, hy]