-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem SameCycle.toList_isRotated {f : Perm α} {x y : α} (h : SameCycle f x y) :
    toList f x ~r toList f y

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

Tactic:
use k.succ

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left✝ : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1)) x = y
⊢ (f.toList x).rotate k.succ = f.toList y

Proof state:
case pos.intro.zero.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : (f ^ 0) x = y
⊢ f.toList x ~r f.toList y

Tactic:
simp only [coe_one, id, pow_zero] at hy

Result:
case pos.intro.zero.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : x = y
⊢ f.toList x ~r f.toList y

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ y ∉ f.support

Tactic:
rwa [← h.mem_support_iff]

Result:
no goals

Proof state:
case pos.intro.zero.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : x = y
⊢ f.toList x ~r f.toList y

Tactic:
simp [hy, IsRotated.refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
⊢ f.toList x ~r f.toList y

Tactic:
by_cases hx : x ∈ f.support

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ f.toList x ~r f.toList y

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ f.toList x ~r f.toList y

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ f.toList x ~r f.toList y

Tactic:
rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ y ∉ f.support

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ f.toList x ~r f.toList y

Tactic:
obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx

Result:
case pos.intro.zero.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : (f ^ 0) x = y
⊢ f.toList x ~r f.toList y

case pos.intro.succ.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left✝ : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1)) x = y
⊢ f.toList x ~r f.toList y

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left✝ : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1)) x = y
⊢ (f.toList x).rotate k.succ = f.toList y

Tactic:
rw [← toList_pow_apply_eq_rotate, hy]

Result:
no goals