ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
⊢ closure {σ, swap x (↑σ x)} = ⊤
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
⊢ closure {σ, swap x (↑σ x)} = ⊤
let H := closure ({σ, swap x (σ x)} : Set (Perm α))
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
⊢ closure {σ, swap x (↑σ x)} = ⊤
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
⊢ closure {σ, swap x (↑σ x)} = ⊤
have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
⊢ closure {σ, swap x (↑σ x)} = ⊤
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
⊢ closure {σ, swap x (↑σ x)} = ⊤
have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
⊢ closure {σ, swap x (↑σ x)} = ⊤
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
⊢ closure {σ, swap x (↑σ x)} = ⊤
have step3 : ∀ y : α, swap x y ∈ H := by
  intro y
  have hx : x ∈ (⊤ : Finset α) := Finset.mem_univ x
  rw [← h2, mem_support] at hx
  have hy : y ∈ (⊤ : Finset α) := Finset.mem_univ y
  rw [← h2, mem_support] at hy
  cases' IsCycle.exists_pow_eq h1 hx hy with n hn
  rw [← hn]
  exact step2 n
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
⊢ {σ | IsSwap σ} ⊆ ↑(closure {σ, swap x (↑σ x)})
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
⊢ closure {σ, swap x (↑σ x)} = ⊤
rw [eq_top_iff, ← closure_isSwap, closure_le]
case intro.intro.intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ τ ∈ ↑(closure {σ, swap x (↑σ x)})
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
⊢ {σ | IsSwap σ} ⊆ ↑(closure {σ, swap x (↑σ x)})
rintro τ ⟨y, z, _, h6⟩
case intro.intro.intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ swap y z ∈ ↑(closure {σ, swap x (↑σ x)})
case intro.intro.intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ τ ∈ ↑(closure {σ, swap x (↑σ x)})
rw [h6]
no goals
case intro.intro.intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ swap y z ∈ ↑(closure {σ, swap x (↑σ x)})
exact step4 y z
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
⊢ swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
⊢ ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
intro n
case zero
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
⊢ swap (↑(σ ^ Nat.zero) x) (↑(σ ^ (Nat.zero + 1)) x) ∈ H

case succ
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
ih : swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap (↑(σ ^ Nat.succ n) x) (↑(σ ^ (Nat.succ n + 1)) x) ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
⊢ swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
induction' n with n ih
no goals
case zero
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
⊢ swap (↑(σ ^ Nat.zero) x) (↑(σ ^ (Nat.zero + 1)) x) ∈ H
exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
case h.e'_4
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
ih : swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap (↑(σ ^ Nat.succ n) x) (↑(σ ^ (Nat.succ n + 1)) x) = σ * swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) * σ⁻¹
case succ
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
ih : swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap (↑(σ ^ Nat.succ n) x) (↑(σ ^ (Nat.succ n + 1)) x) ∈ H
convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
case h.e'_4
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
ih : swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap (↑(σ * σ ^ n) x) (↑(σ * (σ * σ ^ n)) x) = swap (↑σ (↑(σ ^ n) x)) (↑σ (↑(σ * σ ^ n) x))
case h.e'_4
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
ih : swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap (↑(σ ^ Nat.succ n) x) (↑(σ ^ (Nat.succ n + 1)) x) = σ * swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) * σ⁻¹
simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ]
no goals
case h.e'_4
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
n : ℕ
ih : swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap (↑(σ * σ ^ n) x) (↑(σ * (σ * σ ^ n)) x) = swap (↑σ (↑(σ ^ n) x)) (↑σ (↑(σ * σ ^ n) x))
rfl
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
⊢ swap x (↑(σ ^ n) x) ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
intro n
case zero
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap x (↑(σ ^ Nat.zero) x) ∈ H

case succ
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
⊢ swap x (↑(σ ^ n) x) ∈ H
induction' n with n ih
case zero
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ Equiv.refl α ∈ closure {σ, swap x (↑σ x)}
case zero
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ swap x (↑(σ ^ Nat.zero) x) ∈ H
simp only [Nat.zero_eq, pow_zero, coe_one, id_eq, swap_self, Set.mem_singleton_iff]
no goals
case zero
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
⊢ Equiv.refl α ∈ closure {σ, swap x (↑σ x)}
convert H.one_mem
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : x = ↑(σ ^ n) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H

case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
case succ
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
by_cases h5 : x = (σ ^ n) x
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : x = ↑(σ ^ (n + 1)) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H

case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : ¬x = ↑(σ ^ (n + 1)) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : ¬x = ↑(σ ^ (n + 1)) x
⊢ swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) * swap x (↑(σ ^ n) x) * swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : ¬x = ↑(σ ^ (n + 1)) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
no goals
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : ¬x = ↑(σ ^ (n + 1)) x
⊢ swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) * swap x (↑(σ ^ n) x) * swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : x = ↑(σ ^ n) x
⊢ swap x (↑σ x) ∈ H
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : x = ↑(σ ^ n) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
rw [pow_succ, mul_apply, ← h5]
no goals
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : x = ↑(σ ^ n) x
⊢ swap x (↑σ x) ∈ H
exact h4
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : x = ↑(σ ^ (n + 1)) x
⊢ Equiv.refl α ∈ H
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : x = ↑(σ ^ (n + 1)) x
⊢ swap x (↑(σ ^ Nat.succ n) x) ∈ H
rw [← h6, swap_self]
no goals
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x (↑(σ ^ n) x) ∈ H
h5 : ¬x = ↑(σ ^ n) x
h6 : x = ↑(σ ^ (n + 1)) x
⊢ Equiv.refl α ∈ H
exact H.one_mem
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
⊢ swap x y ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
⊢ ∀ (y : α), swap x y ∈ H
intro y
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : x ∈ ⊤
⊢ swap x y ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
⊢ swap x y ∈ H
have hx : x ∈ (⊤ : Finset α) := Finset.mem_univ x
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
⊢ swap x y ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : x ∈ ⊤
⊢ swap x y ∈ H
rw [← h2, mem_support] at hx
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : y ∈ ⊤
⊢ swap x y ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
⊢ swap x y ∈ H
have hy : y ∈ (⊤ : Finset α) := Finset.mem_univ y
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : ↑σ y ≠ y
⊢ swap x y ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : y ∈ ⊤
⊢ swap x y ∈ H
rw [← h2, mem_support] at hy
case intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : ↑σ y ≠ y
n : ℕ
hn : ↑(σ ^ n) x = y
⊢ swap x y ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : ↑σ y ≠ y
⊢ swap x y ∈ H
cases' IsCycle.exists_pow_eq h1 hx hy with n hn
case intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : ↑σ y ≠ y
n : ℕ
hn : ↑(σ ^ n) x = y
⊢ swap x (↑(σ ^ n) x) ∈ H
case intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : ↑σ y ≠ y
n : ℕ
hn : ↑(σ ^ n) x = y
⊢ swap x y ∈ H
rw [← hn]
no goals
case intro
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
y : α
hx : ↑σ x ≠ x
hy : ↑σ y ≠ y
n : ℕ
hn : ↑(σ ^ n) x = y
⊢ swap x (↑(σ ^ n) x) ∈ H
exact step2 n
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
⊢ swap y z ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
⊢ ∀ (y z : α), swap y z ∈ H
intro y z
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap y z ∈ H

case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
⊢ swap y z ∈ H
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
⊢ swap y z ∈ H
by_cases h5 : z = x
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ swap y z ∈ H

case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap y z ∈ H
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
⊢ swap y z ∈ H
by_cases h6 : z = y
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap x y * swap x z * swap x y ∈ H
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap y z ∈ H
rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
no goals
case neg
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap x y * swap x z * swap x y ∈ H
exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap y z ∈ H
rw [h5, swap_comm]
no goals
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H
exact step3 y
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ Equiv.refl α ∈ H
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ swap y z ∈ H
rw [h6, swap_self]
no goals
case pos
ι : Type ?u.2796652
α : Type u_1
β : Type ?u.2796658
inst✝² : DecidableEq α
inst✝¹ : Finite β
inst✝ : Fintype α
σ : Perm α
h1 : IsCycle σ
h2 : support σ = ⊤
x : α
H : Subgroup (Perm α) := closure {σ, swap x (↑σ x)}
h3 : σ ∈ H
h4 : swap x (↑σ x) ∈ H
step1 : ∀ (n : ℕ), swap (↑(σ ^ n) x) (↑(σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x (↑(σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ Equiv.refl α ∈ H
exact H.one_mem