-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    IsCycle (f ^ n) ↔ n.Coprime (orderOf f)

Proof state:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ ((f ^ n) ^ m).support

Tactic:
rw [hm]

Result:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ f.support

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (f ^ n).IsCycle → n.Coprime (orderOf f)

Tactic:
intro h

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ n.Coprime (orderOf f)

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ ¬orderOf f ∣ n

Tactic:
rintro ⟨k, rfl⟩

Result:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
⊢ False

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ n.Coprime (orderOf f)

Tactic:
have hr : support (f ^ n) = support f := by
  rw [hf.support_pow_eq_iff]
  rintro ⟨k, rfl⟩
  refine h.ne_one ?_
  simp [pow_mul, pow_orderOf_eq_one]

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ n.Coprime (orderOf f)

Proof state:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ n.Coprime (orderOf f) → (f ^ n).IsCycle

Tactic:
intro h

Result:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf f = 0 ∨ (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)

Tactic:
rcases this with h | _

Result:
case intro.mp.inl
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h✝ : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h : orderOf f = 0
⊢ n.Coprime (orderOf f)

case intro.mp.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h✝ : (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ orderOf (f ^ n) = orderOf f

Tactic:
rw [h.orderOf, hr, hf.orderOf]

Result:
no goals

Proof state:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ f.support

Tactic:
exact support_pow_le _ n hx

Result:
no goals

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ ((f ^ n) ^ m).IsCycle

Tactic:
rwa [hm]

Result:
no goals

Proof state:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
refine hf'.of_pow fun x hx => ?_

Result:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ ((f ^ n) ^ m).support

Proof state:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ (f ^ n).IsCycle

Tactic:
have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]

Result:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ n.Coprime (orderOf f)

Tactic:
have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf (f ^ n) = orderOf f
⊢ n.Coprime (orderOf f)

Proof state:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf (f ^ n) = orderOf f
⊢ n.Coprime (orderOf f)

Tactic:
rw [orderOf_pow, Nat.div_eq_self] at this

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf f = 0 ∨ (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)

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

Tactic:
rw [hf.support_pow_eq_iff]

Result:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ ¬orderOf f ∣ n

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Tactic:
cases nonempty_fintype β

Result:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Proof state:
case intro.mp.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h✝ : (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)

Tactic:
rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]

Result:
no goals

Proof state:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
⊢ False

Tactic:
refine h.ne_one ?_

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

Proof state:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

Tactic:
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h

Result:
case intro.mpr.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ (f ^ n).IsCycle

Proof state:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Tactic:
constructor

Result:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (f ^ n).IsCycle → n.Coprime (orderOf f)

case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ n.Coprime (orderOf f) → (f ^ n).IsCycle

Proof state:
case intro.mp.inl
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h✝ : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h : orderOf f = 0
⊢ n.Coprime (orderOf f)

Tactic:
exact absurd h (orderOf_pos _).ne'

Result:
no goals

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

Tactic:
simp [pow_mul, pow_orderOf_eq_one]

Result:
no goals