no goals
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ IsCycle (f ^ n)
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
case intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ IsCycle (f ^ n)
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ IsCycle (f ^ n)
cases nonempty_fintype β
case intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
⊢ IsCycle (f ^ n)
case intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ IsCycle (f ^ n)
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'
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ IsCycle (f ^ n)
case intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
⊢ IsCycle (f ^ n)
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime this
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle f
⊢ IsCycle (f ^ n)
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ IsCycle (f ^ n)
have hf'' := hf
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle ((f ^ n) ^ m)
⊢ IsCycle (f ^ n)
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle f
⊢ IsCycle (f ^ n)
rw [← hm] at hf''
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle ((f ^ n) ^ m)
⊢ support (f ^ n) ⊆ support ((f ^ n) ^ m)
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle ((f ^ n) ^ m)
⊢ IsCycle (f ^ n)
refine' hf''.of_pow _
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle ((f ^ n) ^ m)
⊢ support (f ^ n) ⊆ support f
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle ((f ^ n) ^ m)
⊢ support (f ^ n) ⊆ support ((f ^ n) ^ m)
rw [hm]
no goals
case intro.intro
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : Nat.coprime n (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf'' : IsCycle ((f ^ n) ^ m)
⊢ support (f ^ n) ⊆ support f
exact support_pow_le f n
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ Nat.coprime (orderOf f) n
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ Nat.coprime n (orderOf f)
refine' Nat.coprime.symm _
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ Nat.coprime (orderOf f) n
rw [Nat.Prime.coprime_iff_not_dvd hf']
no goals
ι : Type ?u.1631268
α : Type ?u.1631271
β : Type u_1
f✝ g : Perm α
x y : α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Finite β
f : Perm β
hf : IsCycle f
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n
exact Nat.not_dvd_of_pos_of_lt hn hn'