-- Mathlib/GroupTheory/Perm/Closure.lean
theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = univ) (x : α) :
    closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤

Proof state:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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)})

Tactic:
rw [h6]

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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)})

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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 ((σ ^ (n + 1)) x) ∈ H

Tactic:
rw [← h6, swap_self]

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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)})

Tactic:
rintro τ ⟨y, z, _, h6⟩

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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)})

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Tactic:
obtain ⟨n, hn⟩ := IsCycle.exists_pow_eq h1 hx hy

Result:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Tactic:
exact step3 y

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Tactic:
exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Tactic:
exact h4

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Tactic:
intro y z

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Proof state:
case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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 + 1)) x) ((σ ^ (n + 1 + 1)) x) ∈ H

Tactic:
convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)

Result:
case h.e'_5
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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 + 1)) x) ((σ ^ (n + 1 + 1)) x) = σ * swap ((σ ^ n) x) ((σ ^ (n + 1)) x) * σ⁻¹

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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

Tactic:
rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]

Result:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
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