ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x : α
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
cases' exists_pow_eq_self_of_coprime h0 with m hm
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
have h2' : (σ ^ n).support = ⊤ := Eq.trans (support_pow_coprime h0) h2
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
h1' : IsCycle ((σ ^ n) ^ ↑m)
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
h1' : IsCycle (σ ^ n)
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
h1' : IsCycle ((σ ^ n) ^ ↑m)
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
replace h1' : IsCycle (σ ^ n) :=
  h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
h1' : IsCycle (σ ^ n)
⊢ σ ^ n ∈ ↑(closure {σ, swap x (↑(σ ^ n) x)}) ∧ {swap x (↑(σ ^ n) x)} ⊆ ↑(closure {σ, swap x (↑(σ ^ n) x)})
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
h1' : IsCycle (σ ^ n)
⊢ closure {σ, swap x (↑(σ ^ n) x)} = ⊤
rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset]
no goals
case intro
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
h1' : IsCycle (σ ^ n)
⊢ σ ^ n ∈ ↑(closure {σ, swap x (↑(σ ^ n) x)}) ∧ {swap x (↑(σ ^ n) x)} ⊆ ↑(closure {σ, swap x (↑(σ ^ n) x)})
exact
  ⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n,
    Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩
no goals
ι : Type ?u.2958039
α : Type u_1
β : Type ?u.2958045
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : Nat.coprime n (orderOf σ)
h1 : IsCycle σ
h2 : support σ = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : support (σ ^ n) = ⊤
⊢ IsCycle ((σ ^ n) ^ ↑m)
rwa [← hm] at h1