-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.isCycle_pow_pos_of_lt_prime_order [Finite β] {f : Perm β} (hf : IsCycle f)
    (hf' : (orderOf f).Prime) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) : IsCycle (f ^ n)

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n

Tactic:
exact Nat.not_dvd_of_pos_of_lt hn hn'

Result:
no goals

Proof state:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
refine hf''.of_pow ?_

Result:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).support ⊆ ((f ^ n) ^ m).support

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ (orderOf f).Coprime n

Tactic:
rw [Nat.Prime.coprime_iff_not_dvd hf']

Result:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n

Proof state:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ (f ^ n).IsCycle

Tactic:
have hf'' := hf

Result:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : f.IsCycle
⊢ (f ^ n).IsCycle

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ (f ^ n).IsCycle

Tactic:
classical
  cases nonempty_fintype β
  have : n.Coprime (orderOf f) := by
    refine Nat.Coprime.symm ?_
    rw [Nat.Prime.coprime_iff_not_dvd hf']
    exact Nat.not_dvd_of_pos_of_lt hn hn'
  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime this
  have hf'' := hf
  rw [← hm] at hf''
  refine hf''.of_pow ?_
  rw [hm]
  exact support_pow_le f n

Result:
no goals

Proof state:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

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

Result:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : 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
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ (f ^ n).IsCycle

Tactic:
have : n.Coprime (orderOf f) := by
  refine Nat.Coprime.symm ?_
  rw [Nat.Prime.coprime_iff_not_dvd hf']
  exact Nat.not_dvd_of_pos_of_lt hn hn'

Result:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

Proof state:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).support ⊆ ((f ^ n) ^ m).support

Tactic:
rw [hm]

Result:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).support ⊆ f.support

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ n.Coprime (orderOf f)

Tactic:
refine Nat.Coprime.symm ?_

Result:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ (orderOf f).Coprime n

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ (f ^ n).IsCycle

Tactic:
cases nonempty_fintype β

Result:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ (f ^ n).IsCycle

Proof state:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).support ⊆ f.support

Tactic:
exact support_pow_le f n

Result:
no goals

Proof state:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : f.IsCycle
⊢ (f ^ n).IsCycle

Tactic:
rw [← hm] at hf''

Result:
case intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle