-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_toList (f : Perm α) (x : α) : formPerm (toList f x) = f.cycleOf x

Proof state:
case neg.H
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Tactic:
by_cases hy : SameCycle f x y

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : f.SameCycle x y
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
ext y

Result:
case neg.H
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Tactic:
rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_not_mem]

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ y ∉ f.toList x

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : f.SameCycle x y
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Tactic:
obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)

Result:
case pos.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).formPerm ((f ^ k) x) = (f.cycleOf x) ((f ^ k) x)

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (not_mem_support.mpr hx),
  formPerm_nil]

Result:
no goals

Proof state:
case pos.intro.intro.hy
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ f.SameCycle x ((f ^ k) x) ∧ x ∈ f.support

Tactic:
exact ⟨⟨k, rfl⟩, mem_support.mpr hx⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ y ∉ f.toList x

Tactic:
simp [mem_toList_iff, hy]

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).formPerm ((f ^ k) x) = (f.cycleOf x) ((f ^ k) x)

Tactic:
rw [cycleOf_apply_apply_pow_self, List.formPerm_apply_mem_eq_next (nodup_toList f x),
  next_toList_eq_apply, pow_succ', mul_apply]

Result:
case pos.intro.intro.hy
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f ^ k) x ∈ f.toList x

Proof state:
case pos.intro.intro.hy
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f ^ k) x ∈ f.toList x

Tactic:
rw [mem_toList_iff]

Result:
case pos.intro.intro.hy
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ f.SameCycle x ((f ^ k) x) ∧ x ∈ f.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
by_cases hx : f x = x

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ (f.toList x).formPerm = f.cycleOf x

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (f.toList x).formPerm = f.cycleOf x