case intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
⊢ closure {σ, τ} = ⊤
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
h3 : IsSwap τ
⊢ closure {σ, τ} = ⊤
obtain ⟨x, y, h4, h5⟩ := h3
case intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
⊢ closure {σ, τ} = ⊤
case intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
⊢ closure {σ, τ} = ⊤
obtain ⟨i, hi⟩ :=
  h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
    (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
case intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
⊢ closure {σ, swap x (↑(σ ^ i) x)} = ⊤
case intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
⊢ closure {σ, τ} = ⊤
rw [h5, ← hi]
case intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
h : Fintype.card α ∣ i
⊢ x = y
case intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
⊢ closure {σ, swap x (↑(σ ^ i) x)} = ⊤
refine'
  closure_cycle_coprime_swap (Nat.coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 _)) h1 h2 x
case intro.intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
m : ℕ
hm : i = Fintype.card α * m
⊢ x = y
case intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
h : Fintype.card α ∣ i
⊢ x = y
cases' h with m hm
no goals
case intro.intro.intro.intro.intro
ι : Type ?u.3022349
α : Type u_1
β : Type ?u.3022355
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : IsCycle σ
h2 : support σ = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : ↑(σ ^ i) x = y
m : ℕ
hm : i = Fintype.card α * m
⊢ x = y
rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
  one_apply] at hi