-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.pow_eq_pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {a b : ℕ} :
    f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Proof state:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x

Result:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : (f ^ 1) ((f ^ ↑a) x) = (f ^ ↑a) ((f ^ 1) x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b → ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
intro h

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ (b - a) = 1
⊢ f ^ a = f ^ b

Tactic:
rw [pow_sub _ hab, mul_inv_eq_one] at this

Result:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b

Proof state:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
constructor

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b → ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x) → f ^ a = f ^ b

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
⊢ f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
cases nonempty_fintype β

Result:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ a = f ^ b

Tactic:
suffices f ^ (b - a) = 1 by
  rw [pow_sub _ hab, mul_inv_eq_one] at this
  rw [this]

Result:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ (b - a) = 1

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b

Tactic:
rw [this]

Result:
no goals

Proof state:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ (f ^ (b - a)) ((f ^ a) x) = (f ^ a) x

Tactic:
simp only [pow_sub _ hab, Equiv.Perm.coe_mul, Function.comp_apply, inv_apply_self, ← hx']

Result:
no goals

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : f x ≠ x
⊢ (f ^ a) x = (f ^ b) x

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩

Result:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ (f ^ (b - a)) ((f ^ a) x) = (f ^ a) x

Proof state:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : (f ^ 1) ((f ^ ↑a) x) = (f ^ ↑a) ((f ^ 1) x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
simp only [zpow_one, zpow_natCast] at h

Result:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Proof state:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
rw [not_mem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa

Result:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : f x = x
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Proof state:
case intro.mpr.intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
⊢ f ^ a = f ^ b

Tactic:
wlog hab : a ≤ b generalizing a b

Result:
case intro.mpr.intro.intro.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
this : ∀ {a b : ℕ}, (f ^ a) x = (f ^ b) x → a ≤ b → f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ a = f ^ b

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ (b - a) = 1

Tactic:
rw [hf.pow_eq_one_iff]

Result:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Proof state:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x) → f ^ a = f ^ b

Tactic:
rintro ⟨x, hx, hx'⟩

Result:
case intro.mpr.intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
⊢ f ^ a = f ^ b

Proof state:
case intro.mpr.intro.intro.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
this : ∀ {a b : ℕ}, (f ^ a) x = (f ^ b) x → a ≤ b → f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

Tactic:
exact (this hx'.symm (le_of_not_le hab)).symm

Result:
no goals

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Result:
case intro.mp.intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : f x ≠ x
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x