awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
⊢ ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H

Tactic:
have step2 : ∀ n : ℕ, swap x ((σ ^ n) x) ∈ H := by
    intro n
    induction n with
    | zero =>
      simp only [pow_zero, coe_one, id_eq, swap_self]
      convert! H.one_mem
    | succ n ih =>
      by_cases h5 : x = (σ ^ n) x
      · rw [pow_succ', mul_apply, ← h5]
        exact h4
      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
      · rw [← h6, swap_self]
        exact H.one_mem
      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
⊢ Membership.mem (γ := Finset α) univ x

Tactic:
have hx : x ∈ univ := Finset.mem_univ x
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : Membership.mem (γ := Finset α) univ x
⊢ (σ : (a : α) → α) x ≠ x

Tactic:
rw [← h2, mem_support] at hx

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : (σ : (a : α) → α) x ≠ x
⊢ Membership.mem (γ := Finset α) univ y

Tactic:
have hy : y ∈ univ := Finset.mem_univ y
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : (σ : (a : α) → α) x ≠ x
hy : Membership.mem (γ := Finset α) univ y
⊢ (σ : (a : α) → α) y ≠ y

Tactic:
rw [← h2, mem_support] at hy

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : (σ : (a : α) → α) x ≠ x
hy : (σ : (a : α) → α) y ≠ y
obtain : ∀ (n : ℕ) (hn : (σ ^ n : (a : α) → α) x = y), swap x y ∈ H
⊢ swap x y ∈ H

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

Premises used: Equiv.Perm.IsCycle.exists_pow_eq
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : (σ : (a : α) → α) x ≠ x
hy : (σ : (a : α) → α) y ≠ y
n : ℕ
hn : (σ ^ n : (a : α) → α) x = y
rw : swap x ((σ ^ n : (a : α) → α) x) ∈ H
⊢ swap x y ∈ H

Tactic:
rw [← hn]
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : (σ : (a : α) → α) x ≠ x
hy : (σ : (a : α) → α) y ≠ y
n : ℕ
hn : (σ ^ n : (a : α) → α) x = y
⊢ swap x ((σ ^ n : (a : α) → α) x) ∈ H

Tactic:
step2 n
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
y : α
hx : (σ : (a : α) → α) x ≠ x
hy : (σ : (a : α) → α) y ≠ y
n : ℕ
hn : (σ ^ n : (a : α) → α) x = y
⊢ swap x ((σ ^ n : (a : α) → α) x) ∈ H

Tactic:
exact step2 n
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
⊢ ∀ (y : α), swap x y ∈ H

Tactic:
have step3 : ∀ y : α, swap x y ∈ H := by
    intro y
    have hx : x ∈ univ := Finset.mem_univ x
    rw [← h2, mem_support] at hx
    have hy : y ∈ univ := Finset.mem_univ y
    rw [← h2, mem_support] at hy
    obtain ⟨n, hn⟩ := IsCycle.exists_pow_eq h1 hx hy
    rw [← hn]
    exact step2 n
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
pos : ∀ (h5 : z = x), swap y z ∈ H
neg : ∀ (h5 : ¬z = x), swap y z ∈ H
⊢ swap y z ∈ H

Tactic:
by_cases h5 : z = x
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
pos : swap x y ∈ H
⊢ swap y z ∈ H

Tactic:
rw [h5, swap_comm]

Premises used: Equiv.swap_comm
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H

Tactic:
step3 y
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H

Tactic:
exact step3 y
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
pos : ∀ (h6 : z = y), swap y z ∈ H
neg : ∀ (h6 : ¬z = y), swap y z ∈ H
⊢ swap y z ∈ H

Tactic:
by_cases h6 : z = y
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
pos : Equiv.refl α ∈ H
⊢ swap y z ∈ H

Tactic:
rw [h6, swap_self]

Premises used: Equiv.swap_self
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ Equiv.refl α ∈ H

Tactic:
H.one_mem

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ Equiv.refl α ∈ H

Tactic:
exact H.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
neg : swap x y * swap x z * swap x y ∈ H
⊢ swap y z ∈ H

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

Premises used: Equiv.swap_comm, Equiv.swap_mul_swap_mul_swap
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) 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

Tactic:
H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)

Premises used: Set.Mem, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) 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

Tactic:
exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)

Premises used: Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
⊢ ∀ (y z : α), swap y z ∈ H

Tactic:
have step4 : ∀ y z : α, swap y z ∈ H := by
    intro y z
    by_cases h5 : z = x
    · rw [h5, swap_comm]
      exact step3 y
    by_cases h6 : z = y
    · rw [h6, swap_self]
      exact H.one_mem
    rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
rw : {σ : Perm α | σ.IsSwap} ⊆ (↑(closure {σ, swap x ((σ : (a : α) → α) x)}) : Set (Perm α))
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤

Tactic:
rw [eq_top_iff, ← closure_isSwap, closure_le]

Premises used: Equiv.Perm.closure_isSwap, eq_top_iff, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) 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
rw : swap y z ∈ (↑(closure {σ, swap x ((σ : (a : α) → α) x)}) : Set (Perm α))
⊢ τ ∈ (↑(closure {σ, swap x ((σ : (a : α) → α) x)}) : Set (Perm α))

Tactic:
rw [h6]
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) 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 ((σ : (a : α) → α) x)}) : Set (Perm α))

Tactic:
step4 y z

Premises used: Set.Mem
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
step1 :
  ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
step2 : ∀ (n : ℕ), swap x ((σ ^ n : (a : α) → α) 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 ((σ : (a : α) → α) x)}) : Set (Perm α))

Tactic:
exact step4 y z
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
rw :
  ∀ (h0 : n.Coprime (orderOf σ)) (h1 : σ.IsCycle) (h2 : σ.support = univ) (x : α),
    Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤

Tactic:
rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0

Premises used: Finset.card_univ, Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
obtain : ∀ (m : ℕ) (hm : (σ ^ n) ^ m = σ), Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤

Tactic:
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h0

Premises used: exists_pow_eq_self_of_coprime
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ (σ ^ n).support = univ

Tactic:
have h2' : (σ ^ n).support = univ := Eq.trans (support_pow_coprime h0) h2
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h1 : ((σ ^ n) ^ m).IsCycle) (hm : (σ ^ n) ^ m = σ) (h2' : (σ ^ n).support = univ),
    (HPow.hPow (β := ℤ) (σ ^ n) (↑m : ℤ)).IsCycle
⊢ (HPow.hPow (β := ℤ) (σ ^ n) (↑m : ℤ)).IsCycle

Tactic:
rwa [← hm] at h1
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
⊢ (HPow.hPow (β := ℤ) (σ ^ n) (↑m : ℤ)).IsCycle

Tactic:
have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
h1' : (HPow.hPow (β := ℤ) (σ ^ n) (↑m : ℤ)).IsCycle
⊢ (σ ^ n).IsCycle

Tactic:
replace h1' : IsCycle (σ ^ n) :=
    h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
h1' : (σ ^ n).IsCycle
rw :
  σ ^ n ∈ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α)) ∧
    {swap x ((σ ^ n : (a : α) → α) x)} ⊆ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α))
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤

Tactic:
rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]

Premises used: eq_top_iff, Subgroup.closure_le, Set.insert_subset_iff, Equiv.Perm.closure_cycle_adjacent_swap
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
h1' : (σ ^ n).IsCycle
⊢ σ ^ n ∈ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α)) ∧
    {swap x ((σ ^ n : (a : α) → α) x)} ⊆ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α))

Tactic:
⟨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 _)))⟩

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, Subgroup.closure, Set.mem_insert_of_mem, Subgroup.subset_closure, And.intro, Set.mem_insert, Subgroup.pow_mem
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
h1' : (σ ^ n).IsCycle
⊢ σ ^ n ∈ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α)) ∧
    {swap x ((σ ^ n : (a : α) → α) x)} ⊆ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α))

Tactic:
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 _)))⟩
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
h3 : τ.IsSwap
obtain : ∀ (x y : α) (h4 : x ≠ y) (h5 : τ = swap x y), Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤

Tactic:
obtain ⟨x, y, h4, h5⟩ := h3
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
obtain : ∀ (i : ℕ) (hi : (σ ^ i : (a : α) → α) x = y), Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤

Tactic:
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)))

Premises used: Iff.mpr, Finset.mem_univ, Equiv.Perm.IsCycle.exists_pow_eq, Equiv.Perm.mem_support, Finset.ext_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
rw : Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ i : (a : α) → α) x)}) ⊤
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤

Tactic:
rw [h5, ← hi]
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ i : (a : α) → α) x)}) ⊤

Tactic:
closure_cycle_coprime_swap
    (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 ?_)) h1 h2 x

Premises used: Iff.mpr, Nat.Coprime.symm, Equiv.Perm.closure_cycle_coprime_swap, Nat.Prime.coprime_iff_not_dvd