-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem SameCycle.exists_pow_eq [DecidableEq α] [Fintype α] (f : Perm α) (h : SameCycle f x y) :
    ∃ i : ℕ, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Proof state:
case pos.intro.intro.zero.refine_1
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ 0 < #(f.cycleOf x).support

Tactic:
refine zero_lt_one.trans (one_lt_card_support_of_ne_one ?_)

Result:
case pos.intro.intro.zero.refine_1
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ f.cycleOf x ≠ 1

Proof state:
case pos.intro.intro.zero.refine_2
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : x = y
⊢ (f ^ #(f.cycleOf x).support) x = y

Tactic:
subst hk'

Result:
case pos.intro.intro.zero.refine_2
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
⊢ (f ^ #(f.cycleOf x).support) x = x

Proof state:
case pos.intro.intro
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k < #(f.cycleOf x).support
hk' : (f ^ k) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
rcases k with - | k

Result:
case pos.intro.intro.zero
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

case pos.intro.intro.succ
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Proof state:
case pos.intro.intro.zero
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
refine ⟨#(f.cycleOf x).support, ?_, self_le_add_right _ _, ?_⟩

Result:
case pos.intro.intro.zero.refine_1
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ 0 < #(f.cycleOf x).support

case pos.intro.intro.zero.refine_2
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ (f ^ #(f.cycleOf x).support) x = y

Proof state:
case pos.intro.intro.zero.refine_1
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ f.cycleOf x ≠ 1

Tactic:
simpa using hx

Result:
no goals

Proof state:
case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ (f ^ 1) x = y

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case neg.intro
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∉ f.support
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x

Proof state:
case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
refine ⟨1, zero_lt_one, by simp, ?_⟩

Result:
case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ (f ^ 1) x = y

Proof state:
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ 1 ≤ #(f.cycleOf x).support + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ 0 < k + 1

Tactic:
simp

Result:
no goals

Proof state:
case neg.intro
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∉ f.support
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x

Tactic:
rw [not_mem_support] at hx

Result:
case neg.intro
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : f x = x
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x

Proof state:
case pos.intro.intro.succ
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩

Result:
no goals

Proof state:
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
by_cases hx : x ∈ f.support

Result:
case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Proof state:
case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx

Result:
case pos.intro.intro
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k < #(f.cycleOf x).support
hk' : (f ^ k) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Proof state:
case pos.intro.intro.zero.refine_2
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ (f ^ #(f.cycleOf x).support) x = y

Tactic:
simp only [pow_zero, coe_one, id_eq] at hk'

Result:
case pos.intro.intro.zero.refine_2
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : x = y
⊢ (f ^ #(f.cycleOf x).support) x = y

Proof state:
case neg.intro
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : f x = x
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]

Result:
no goals

Proof state:
case pos.intro.intro.zero.refine_2
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
⊢ (f ^ #(f.cycleOf x).support) x = x

Tactic:
rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
  pow_orderOf_eq_one, one_apply]

Result:
no goals