awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have step1 : ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 α)
⊢ swap x ((HPow.hPow (β := ℕ) σ 0 : (a : α) → α) x) ∈ H
have zero : Equiv.refl α ∈ H
Tactic: simp only [pow_zero, coe_one, id_eq, swap_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
have pos : ∀ (h5 : x = (σ ^ n : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
Tactic: by_cases h5 : x = (σ ^ n) x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
have neg : ∀ (h5 : ¬x = (σ ^ n : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
Tactic: by_cases h5 : x = (σ ^ n) x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
have pos : ∀ (h6 : x = (σ ^ (n + 1) : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
Tactic: by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
have neg : ∀ (h6 : ¬x = (σ ^ (n + 1) : (a : α) → α) x), swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
Tactic: by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
have pos : Equiv.refl α ∈ H
Tactic: rw [← h6, swap_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x ((σ ^ (n + 1) : (a : α) → α) x) ∈ H
have 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
Tactic: rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
have zero : swap x ((HPow.hPow (β := ℕ) σ 0 : (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)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x ((σ ^ n : (a : α) → α) x) ∈ H
have succ : ∀ (n : ℕ) (ih : swap x ((σ ^ n : (a : α) → α) x) ∈ H), swap x ((σ ^ (n + 1) : (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)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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 α)
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have step2 : ∀ (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
have hx : Membership.mem (γ := Finset α) univ x
Tactic: have hx : x ∈ univ := Finset.mem_univ x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ swap x y ∈ H
have hx₁ : (σ : (a : α) → α) x ≠ x
Tactic: rw [← h2, mem_support] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ swap x y ∈ H
have hy : Membership.mem (γ := Finset α) univ y
Tactic: have hy : y ∈ univ := Finset.mem_univ y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ swap x y ∈ H
have hy₁ : (σ : (a : α) → α) y ≠ y
Tactic: rw [← h2, mem_support] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap x y ∈ H
have obtain : ∀ (n : ℕ) (hn : (σ ^ n : (a : α) → α) x = y), swap x y ∈ H
Tactic: obtain ⟨n, hn⟩ := IsCycle.exists_pow_eq h1 hx hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 y ∈ H
have rw : swap x ((σ ^ n : (a : α) → α) x) ∈ H
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have step3 : ∀ (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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
have pos : ∀ (h5 : z = x), swap y z ∈ H
Tactic: by_cases h5 : z = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap y z ∈ H
have neg : ∀ (h5 : ¬z = x), swap y z ∈ H
Tactic: by_cases h5 : z = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 y z ∈ H
have pos : swap x y ∈ H
Tactic: rw [h5, swap_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 y z ∈ H
have pos : ∀ (h6 : z = y), swap y z ∈ H
Tactic: by_cases h6 : z = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ swap y z ∈ H
have neg : ∀ (h6 : ¬z = y), swap y z ∈ H
Tactic: by_cases h6 : z = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 y z ∈ H
have pos : Equiv.refl α ∈ H
Tactic: rw [h6, swap_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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 y z ∈ H
have neg : swap x y * swap x z * swap x y ∈ H
Tactic: rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have step4 : ∀ (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ : (a : α) → α) x)}) ⊤
have rw : {σ : Perm α | σ.IsSwap} ⊆ (↑(closure {σ, swap x ((σ : (a : α) → α) x)}) : Set (Perm α))
Tactic: rw [eq_top_iff, ← closure_isSwap, closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ τ ∈ (↑(closure {σ, swap x ((σ : (a : α) → α) x)}) : Set (Perm α))
have rw : swap y z ∈ (↑(closure {σ, swap x ((σ : (a : α) → α) x)}) : Set (Perm α))
Tactic: rw [h6]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
have rw : ∀ (h0 : n.Coprime (orderOf σ)) (h1 : σ.IsCycle) (h2 : σ.support = univ) (x : α),
  Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
Tactic: rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
Cleared hypotheses: h0, h1, h2, x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
have obtain : ∀ (m : ℕ) (hm : (σ ^ n) ^ m = σ), Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
Tactic: obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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 = σ
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
have h2' : (σ ^ n).support = univ
Tactic: have h2' : (σ ^ n).support = univ := Eq.trans (support_pow_coprime h0) h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
have rwa : ∀ (h1 : ((σ ^ n) ^ m).IsCycle) (hm : (σ ^ n) ^ m = σ) (h2' : (σ ^ n).support = univ),
  (HPow.hPow (β := ℤ) (σ ^ n) (↑m : ℤ)).IsCycle
Tactic: rwa [← hm] at h1
Cleared hypotheses: h1, hm, h2'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
have h1' : (HPow.hPow (β := ℤ) (σ ^ n) (↑m : ℤ)).IsCycle
Tactic: have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (hypothesis)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
have h1'₁ : (σ ^ n).IsCycle
Tactic: replace h1' : IsCycle (σ ^ n) :=
    h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
Cleared hypotheses: h1'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
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
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) ⊤
have rw : σ ^ n ∈ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α)) ∧
  {swap x ((σ ^ n : (a : α) → α) x)} ⊆ (↑(closure {σ, swap x ((σ ^ n : (a : α) → α) x)}) : Set (Perm α))
Tactic: rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]