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

Proof state:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case neg.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k)) x = x
⊢ f ^ (orderOf f * k) = 1

Proof state:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : ¬(f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
rw [hf.support_pow_eq_iff, Classical.not_not] at h

Result:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1

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

Tactic:
constructor

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

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

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

Tactic:
rintro ⟨x, hx, hx'⟩

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

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

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

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

Proof state:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : (f ^ n) x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
contradiction

Result:
no goals

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

Tactic:
cases nonempty_fintype β

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

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

Tactic:
by_cases h : support (f ^ n) = support f

Result:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : ¬(f ^ n).support = f.support
⊢ f ^ n = 1

Proof state:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
rw [← mem_support, ← h, mem_support] at hx

Result:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : (f ^ n) x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

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

Tactic:
intro h

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

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

Tactic:
exact ⟨x, hx, by simp [h]⟩

Result:
no goals

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

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k)) x = x
⊢ f ^ (orderOf f * k) = 1

Tactic:
rw [pow_mul, pow_orderOf_eq_one, one_pow]

Result:
no goals