awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
pos : 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!
pos₁ :
  (Fintype.card α)! =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
⊢ (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m}

Tactic:
apply Nat.div_eq_of_eq_mul_left

Premises used: Nat.div_eq_of_eq_mul_left
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ 0 < m.prod

Tactic:
have : 0 < m.prod := Multiset.prod_pos <| fun a ha => zero_lt_two.trans_le (hm.2 a ha)
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
this : 0 < m.prod
⊢ 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!

Tactic:
positivity
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
pos : (Fintype.card α)! = if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
pos₁ pos₂ : (Fintype.card α)! = (Fintype.card α)!
⊢ (Fintype.card α)! =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)

Tactic:
rw [card_of_cycleType_mul_eq, if_pos hm]

Premises used: Equiv.Perm.card_of_cycleType_mul_eq, if_pos
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0

Tactic:
(card_of_cycleType_eq_zero_iff α).mpr hm

Premises used: Iff.mpr, Equiv.Perm.card_of_cycleType_eq_zero_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0

Tactic:
exact (card_of_cycleType_eq_zero_iff α).mpr hm

Premises used: Iff.mpr, Equiv.Perm.card_of_cycleType_eq_zero_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
⊢ n ≠ 0

Tactic:
have hn₀ : n ≠ 0 := by lia
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
rw : n ! = n * (n - 1)!
rw₁ rw₂ : n ! = n !
⊢ n ! = (n - 1)! * n

Tactic:
rw [mul_comm, mul_factorial_pred hn₀]

Premises used: mul_comm, Nat.mul_factorial_pred
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ n ! = (n - 1)! * n

Tactic:
have aux : n ! = (n - 1)! * n := by rw [mul_comm, mul_factorial_pred hn₀]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
rw : Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} * (n * (card α - n)!) = (card α)!
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} = (n - 1)! * (card α).choose n

Tactic:
rw [mul_comm, ← Nat.mul_left_inj hn₀, mul_assoc, ← aux, ← Nat.mul_left_inj (factorial_ne_zero _),
    Nat.choose_mul_factorial_mul_factorial hα, mul_assoc]

Premises used: mul_assoc, Nat.choose_mul_factorial_mul_factorial, Nat.factorial_ne_zero, Nat.mul_left_inj, mul_comm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} * (n * (card α - n)!) = (card α)!

Tactic:
simpa [ite_and, if_pos hα, if_pos hn', mul_comm _ n, mul_assoc]
    using card_of_cycleType_mul_eq α {n}

Premises used: Equiv.Perm.card_of_cycleType_mul_eq, mul_assoc, if_pos, mul_comm, ite_and, Singleton.singleton
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
β : Type u_3
inst : Finite β
intro : ∀ (val : Fintype β), Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤
⊢ Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
β : Type u_3
inst : Finite β
val : Fintype β
⊢ Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤

Tactic:
top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

Premises used: Equiv.Perm.closure_isSwap, ge_of_eq, Subgroup.closure_mono, top_le_iff, Iff.mp, Equiv.Perm.IsSwap.isCycle, le_trans
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
β : Type u_3
inst : Finite β
val : Fintype β
⊢ Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤

Tactic:
exact
      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

Premises used: Equiv.Perm.closure_isSwap, ge_of_eq, Subgroup.closure_mono, top_le_iff, Iff.mp, Equiv.Perm.IsSwap.isCycle, le_trans
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
β : Type u_3
inst : Finite β
intro : ∀ (val : Fintype β), Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤
⊢ Eq.{u_3 + 1} (α := Subgroup (Perm β)) (closure {σ : Perm β | σ.IsCycle}) ⊤

Tactic:
classical
    cases nonempty_fintype β
    exact
      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

Premises used: Equiv.Perm.closure_isSwap, ge_of_eq, Subgroup.closure_mono, nonempty_fintype, top_le_iff, Iff.mp, Equiv.Perm.IsSwap.isCycle, le_trans
-- 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)}
⊢ σ ∈ H

Tactic:
have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
-- 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
⊢ swap x ((σ : (a : α) → α) x) ∈ H

Tactic:
have h4 : swap x (σ x) ∈ H := 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 α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x ((σ : (a : α) → α) x)}
h3 : σ ∈ H
h4 : swap x ((σ : (a : α) → α) x) ∈ H
⊢ Membership.mem (α := Perm α) H
    (swap ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ((σ ^ HAdd.hAdd (α := ℕ) 0 1 : (a : α) → α) x) : Perm α)

Tactic:
subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Premises used: Set.mem_singleton, Set.Mem, Set.mem_insert_of_mem, Subgroup.subset_closure
-- 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
⊢ Membership.mem (α := Perm α) H
    (swap ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ((σ ^ HAdd.hAdd (α := ℕ) 0 1 : (a : α) → α) x) : Perm α)

Tactic:
exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Premises used: Set.mem_singleton, Set.mem_insert_of_mem, Subgroup.subset_closure
-- 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
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
⊢ HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹ ∈ H

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

Premises used: Subgroup.inv_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
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
h :
  swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹
⊢ Membership.mem (α := Perm α) H (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)

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

Premises used: Subgroup.inv_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
n : ℕ
ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
h :
  swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (α := Perm α)
        (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α))
            ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
          Perm α)
        σ *
      σ⁻¹
h₁ :
  Eq (α := Perm α) (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
    (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ ^ (n + 1) : (a : α) → α) x : α)) :
      Perm α)
h₂ :
  Eq (α := Perm α) (swap ((σ * σ ^ n : (a : α) → α) x) ((σ * (σ * σ ^ n) : (a : α) → α) x) : Perm α)
    (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α)) ((σ : (a : α) → α) ((σ * σ ^ n : (a : α) → α) x : α)) :
      Perm α)
h₃ :
  Eq (α := Perm α)
    (swap (comp (β := α) (⇑σ : (a : α) → α) (⇑(σ ^ n) : (a : α) → α) x)
        (comp (β := α) (⇑σ : (a : α) → α) (comp (β := α) (⇑σ : (a : α) → α) (⇑(σ ^ n) : (a : α) → α)) x) :
      Perm α)
    (swap ((σ : (a : α) → α) ((σ ^ n : (a : α) → α) x : α))
        ((σ : (a : α) → α) (comp (β := α) (⇑σ : (a : α) → α) (⇑(σ ^ n) : (a : α) → α) x)) :
      Perm α)
⊢ swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) =
    HMul.hMul (β := Perm α) σ (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) * σ⁻¹

Tactic:
simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]

Premises used: mul_inv_cancel_right, Equiv.Perm.coe_mul, Equiv.mul_swap_eq_swap_mul, Function.comp_apply, pow_succ'
-- 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
n : ℕ
zero :
  Membership.mem (α := Perm α) H
    (swap ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ((σ ^ HAdd.hAdd (α := ℕ) 0 1 : (a : α) → α) x) : Perm α)
succ :
  ∀ (n : ℕ)
    (ih : Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)),
    Membership.mem (α := Perm α) H (swap ((σ ^ (n + 1) : (a : α) → α) x) ((σ ^ (n + 1 + 1) : (a : α) → α) x) : Perm α)
⊢ Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)

Tactic:
induction n with
    | zero => exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    | succ n ih =>
      convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]

Premises used: mul_inv_cancel_right, Set.mem_singleton, Equiv.Perm.coe_mul, Set.mem_insert_of_mem, Equiv.mul_swap_eq_swap_mul, Subgroup.subset_closure, Function.comp_apply, pow_succ'
-- 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
⊢ ∀ (n : ℕ), Membership.mem (α := Perm α) H (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)

Tactic:
have step1 : ∀ n : ℕ, swap ((σ ^ n) x) ((σ ^ (n + 1) : Perm α) x) ∈ H := by
    intro n
    induction n with
    | zero => exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    | succ n ih =>
      convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
-- 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 α)
zero : Equiv.refl α ∈ H
⊢ swap x ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ∈ H

Tactic:
simp only [pow_zero, coe_one, id_eq, swap_self]

Premises used: Equiv.Perm.coe_one, pow_zero, Equiv.swap_self, id_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 α)
⊢ 1 ∈ H

Tactic:
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 α)
⊢ Equiv.refl α ∈ H

Tactic:
convert! 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 α)
n : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
pos : ∀ (h5 : x = (σ ^ n : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
neg : ∀ (h5 : ¬x = (σ ^ n : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H

Tactic:
by_cases h5 : x = (σ ^ n) x

Premises used: HPow.hPow, DFunLike.coe
-- 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 : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : x = (σ ^ n : (a : α) → α) x
pos : swap x ((σ : (a : α) → α) x) ∈ H
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H

Tactic:
rw [pow_succ', mul_apply, ← h5]

Premises used: Equiv.Perm.mul_apply, pow_succ'
-- 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 : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : x = (σ ^ n : (a : α) → α) x
⊢ swap x ((σ : (a : α) → α) x) ∈ H

Tactic:
h4
-- 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 : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : x = (σ ^ n : (a : α) → α) x
⊢ swap x ((σ : (a : α) → α) x) ∈ H

Tactic:
exact h4
-- 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 : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
pos : ∀ (h6 : x = (σ ^ (n + 1) : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
neg : ∀ (h6 : ¬x = (σ ^ (n + 1) : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H

Tactic:
by_cases h6 : x = (σ ^ (n + 1) : Perm α) x

Premises used: HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- 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 : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
h6 : x = (σ ^ (n + 1) : (a : α) → α) x
pos : Equiv.refl α ∈ H
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ 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 α)
n : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
h6 : x = (σ ^ (n + 1) : (a : α) → α) x
⊢ 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 α)
n : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
h6 : x = (σ ^ (n + 1) : (a : α) → α) x
⊢ 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 α)
n : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
h6 : ¬x = (σ ^ (n + 1) : (a : α) → α) x
neg :
  HMul.hMul (β := Perm α)
      (HMul.hMul (α := Perm α) (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
        (swap x ((σ ^ n : (a : α) → α) x)))
      (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) ∈
    H
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H

Tactic:
rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]

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 α)
n : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
h6 : ¬x = (σ ^ (n + 1) : (a : α) → α) x
⊢ HMul.hMul (β := Perm α)
      (HMul.hMul (α := Perm α) (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
        (swap x ((σ ^ n : (a : α) → α) x)))
      (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) ∈
    H

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

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 α)
n : ℕ
ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H
h5 : ¬x = (σ ^ n : (a : α) → α) x
h6 : ¬x = (σ ^ (n + 1) : (a : α) → α) x
⊢ HMul.hMul (β := Perm α)
      (HMul.hMul (α := Perm α) (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α)
        (swap x ((σ ^ n : (a : α) → α) x)))
      (swap ((σ ^ n : (a : α) → α) x) ((σ ^ (n + 1) : (a : α) → α) x) : Perm α) ∈
    H

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

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 α)
n : ℕ
zero : swap x ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ∈ H
succ : ∀ (n : ℕ) (ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
⊢ swap x ((σ ^ n : (a : α) → α) x) ∈ H

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

Premises used: Equiv.swap_comm, Equiv.Perm.coe_one, Subgroup.one_mem, pow_zero, HPow.hPow, HAdd.hAdd, Equiv.swap_self, Equiv.Perm.mul_apply, OfNat.ofNat, DFunLike.coe, pow_succ', id_eq