-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem mem_toList_iff {y : α} : y ∈ toList p x ↔ SameCycle p x y ∧ x ∈ p.support

Proof state:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support.card ≤ n

Tactic:
rw [← support_cycleOf_eq_nil_iff] at hx

Result:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : (p.cycleOf x).support = ∅
⊢ (p.cycleOf x).support.card ≤ n

Proof state:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : (p.cycleOf x).support = ∅
⊢ (p.cycleOf x).support.card ≤ n

Tactic:
simp [hx]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m) x = y) → p.SameCycle x y ∧ x ∈ p.support

Tactic:
rintro ⟨n, hx, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ p.SameCycle x ((p ^ n) x) ∧ x ∈ p.support

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
h : p.SameCycle x y
hx : x ∈ p.support
⊢ ∃ m < (p.cycleOf x).support.card, (p ^ m) x = y

Tactic:
simpa using h.exists_pow_eq_of_mem_support hx

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m) x = y) → p.SameCycle x y ∧ x ∈ p.support

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ p.SameCycle x y ∧ x ∈ p.support → ∃ m < (p.cycleOf x).support.card, (p ^ m) x = y

Proof state:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ x ∈ p.support

Tactic:
contrapose! hx

Result:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support.card ≤ n

Proof state:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ p.SameCycle x y ∧ x ∈ p.support → ∃ m < (p.cycleOf x).support.card, (p ^ m) x = y

Tactic:
rintro ⟨h, hx⟩

Result:
case mpr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
h : p.SameCycle x y
hx : x ∈ p.support
⊢ ∃ m < (p.cycleOf x).support.card, (p ^ m) x = y

Proof state:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ p.SameCycle x ((p ^ n) x) ∧ x ∈ p.support

Tactic:
refine ⟨⟨n, rfl⟩, ?_⟩

Result:
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ x ∈ p.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support

Tactic:
simp only [toList, mem_iterate, iterate_eq_pow, eq_comm (a := y)]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support