α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y) ↔ SameCycle p x y ∧ x ∈ support p
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ y ∈ toList p x ↔ SameCycle p x y ∧ x ∈ support p
simp only [toList, mem_range, mem_map]
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y) → SameCycle p x y ∧ x ∈ support p

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ SameCycle p x y ∧ x ∈ support p → ∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y) ↔ SameCycle p x y ∧ x ∈ support p
constructor
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < Finset.card (support (cycleOf p x))
⊢ SameCycle p x (↑(p ^ n) x) ∧ x ∈ support p
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y) → SameCycle p x y ∧ x ∈ support p
rintro ⟨n, hx, rfl⟩
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < Finset.card (support (cycleOf p x))
⊢ x ∈ support p
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < Finset.card (support (cycleOf p x))
⊢ SameCycle p x (↑(p ^ n) x) ∧ x ∈ support p
refine' ⟨⟨n, rfl⟩, _⟩
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : ¬x ∈ support p
⊢ Finset.card (support (cycleOf p x)) ≤ n
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < Finset.card (support (cycleOf p x))
⊢ x ∈ support p
contrapose! hx
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : support (cycleOf p x) = ∅
⊢ Finset.card (support (cycleOf p x)) ≤ n
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : ¬x ∈ support p
⊢ Finset.card (support (cycleOf p x)) ≤ n
rw [← support_cycleOf_eq_nil_iff] at hx
no goals
case mp.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : support (cycleOf p x) = ∅
⊢ Finset.card (support (cycleOf p x)) ≤ n
simp [hx]
case mpr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
h : SameCycle p x y
hx : x ∈ support p
⊢ ∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ SameCycle p x y ∧ x ∈ support p → ∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y
rintro ⟨h, hx⟩
no goals
case mpr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
h : SameCycle p x y
hx : x ∈ support p
⊢ ∃ a, a < Finset.card (support (cycleOf p x)) ∧ ↑(p ^ a) x = y
simpa using h.exists_pow_eq_of_mem_support hx