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

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
α : 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
by_cases hx : x ∈ f.support
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

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
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
obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx
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
⊢ rotate (toList f x) (Nat.succ k) = toList f y
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
use k.succ
no goals
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
⊢ rotate (toList f x) (Nat.succ k) = toList f y
rw [← toList_pow_apply_eq_rotate, hy]
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
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
simp only [coe_one, id.def, pow_zero, Nat.zero_eq] at hy
no goals
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
simp [hy, IsRotated.refl]
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
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
rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]
no goals
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
rwa [← h.mem_support_iff]