awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
mpr :
  ∀ (x : α),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
              (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) :
            (a : α) → α)
          x :
        α)
⊢ g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
mpr :
  Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
            (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
simp only [coe_mul, Function.comp_apply]

Premises used: Equiv.Perm.coe_mul, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
pos :
  ∀ (h : x ∈ g.support),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((swap a ((g : (a : α) → α) a) : (a : α) → α)
          (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
        α)
neg :
  ∀ (h : x ∉ g.support),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((swap a ((g : (a : α) → α) a) : (a : α) → α)
          (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
        α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)

Tactic:
by_cases h : x ∈ g.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∈ g.support
⊢ x = a ∨ x = (g : (a : α) → α) a ∨ x = (g : (a : α) → α) ((g : (a : α) → α) a : α)

Tactic:
simp only [ha', Finset.mem_insert, Finset.mem_singleton] at h

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x = a ∨ x = (g : (a : α) → α) a ∨ x = (g : (a : α) → α) ((g : (a : α) → α) a : α)
pos :
  ∀ (ha : x ∈ g.support)
    (ha' :
      g.support =
        insert x
          (insert (α := α) ((g : (a : α) → α) x : α)
            (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α))))
    (ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((swap x ((g : (a : α) → α) x) : (a : α) → α)
          (((swap ((g : (a : α) → α) x) ((g : (a : α) → α) ((g : (a : α) → α) x : α)) : Perm α) : (a : α) → α) x : α) :
        α)
pos₁ :
  Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) a : α) :
          α) :
      α)
pos₂ :
  Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) :
          α) :
      α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)

Tactic:
rcases h with rfl | (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' :
  g.support =
    insert x
      (insert (α := α) ((g : (a : α) → α) x : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α)))
ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup
⊢ x ≠ (g : (a : α) → α) x

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' :
  g.support =
    insert x
      (insert (α := α) ((g : (a : α) → α) x : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α)))
ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup
⊢ x ≠ (g : (a : α) → α) ((g : (a : α) → α) x : α)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' :
  g.support =
    insert x
      (insert (α := α) ((g : (a : α) → α) x : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α)))
ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup
pos : Eq (α := α) ((g : (a : α) → α) x : α) ((swap x ((g : (a : α) → α) x) : (a : α) → α) x : α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap x ((g : (a : α) → α) x) : (a : α) → α)
        (((swap ((g : (a : α) → α) x) ((g : (a : α) → α) ((g : (a : α) → α) x : α)) : Perm α) : (a : α) → α) x : α) :
      α)

Tactic:
rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' :
  g.support =
    insert x
      (insert (α := α) ((g : (a : α) → α) x : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α)))
ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((swap x ((g : (a : α) → α) x) : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ (g : (a : α) → α) ((g : (a : α) → α) a : α) ≠ a

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ Ne (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) ((g : (a : α) → α) a : α)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
pos :
  Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
pos₁ pos₂ :
  Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) a : α) :
          α) :
      α)

Tactic:
rw [swap_apply_left, swap_apply_of_ne_of_ne (by grind) (by grind)]

Premises used: Equiv.swap_apply_of_ne_of_ne, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
pos : (g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) = a
⊢ Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) :
          α) :
      α)

Tactic:
simp only [swap_apply_right]

Premises used: Equiv.swap_apply_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
this : (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a
⊢ (g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) = a

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
pos : (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a
⊢ (g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) = a

Tactic:
suffices (g ^ 3) a = a by simpa
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a

Tactic:
simp [← hg3.orderOf]

Premises used: Equiv.Perm.IsThreeCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
⊢ x ≠ (g : (a : α) → α) a

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
⊢ x ≠ (g : (a : α) → α) ((g : (a : α) → α) a : α)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
neg : Eq (α := α) ((g : (a : α) → α) x : α) ((swap a ((g : (a : α) → α) a) : (a : α) → α) x : α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)

Tactic:
rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
⊢ x ≠ a

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
neg : (g : (a : α) → α) x = x
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((swap a ((g : (a : α) → α) a) : (a : α) → α) x : α)

Tactic:
rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∉ g.support
⊢ (g : (a : α) → α) x = x

Tactic:
simpa [notMem_support] using h

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
pos :
  ∀ (bc : b = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
neg :
  ∀ (bc : ¬b = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)

Tactic:
by_cases bc : b = c
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b = c
pos :
  ∀ (ac : a ≠ b), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a b)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)

Tactic:
subst bc
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab ac : a ≠ b
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a b)

Tactic:
simp [one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : ¬b = c
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)

Tactic:
subset_closure (isThreeCycle_swap_mul_swap_same ab ac bc)

Premises used: Subgroup.subset_closure, Equiv.Perm.isThreeCycle_swap_mul_swap_same
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : ¬b = c
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a c)

Tactic:
exact subset_closure (isThreeCycle_swap_mul_swap_same ab ac bc)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsSwap
hτ : τ.IsSwap
obtain :
  ∀ (a b : α) (ab : a ≠ b),
    Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * τ)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (σ * τ)

Tactic:
obtain ⟨a, b, ab, rfl⟩ := hσ

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
hτ : τ.IsSwap
a b : α
ab : a ≠ b
obtain :
  ∀ (c d : α) (cd : c ≠ d),
    Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * τ)

Tactic:
obtain ⟨c, d, cd, rfl⟩ := hτ

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
pos :
  ∀ (ac : a = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
neg :
  ∀ (ac : ¬a = c), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)

Tactic:
by_cases ac : a = c
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : a = c
pos :
  ∀ (cd : a ≠ d), Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)

Tactic:
subst ac
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
d : α
cd : a ≠ d
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a d)

Tactic:
swap_mul_swap_same_mem_closure_three_cycles ab cd

Premises used: Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
d : α
cd : a ≠ d
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap a d)

Tactic:
exact swap_mul_swap_same_mem_closure_three_cycles ab cd

Premises used: Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)

Tactic:
simp [swap_comm c a, mul_assoc]

Premises used: Equiv.swap_comm, mul_assoc
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)

Tactic:
have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d) := by
    simp [swap_comm c a, mul_assoc]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
neg :
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle})
    (swap a b * swap a c * (swap c a * swap c d))
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (swap a b * swap c d)

Tactic:
rw [h']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle})
    (swap a b * swap a c * (swap c a * swap c d))

Tactic:
mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
      (swap_mul_swap_same_mem_closure_three_cycles (Ne.symm ac) cd)

Premises used: Ne.symm, Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle})
    (swap a b * swap a c * (swap c a * swap c d))

Tactic:
exact
    mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
      (swap_mul_swap_same_mem_closure_three_cycles (Ne.symm ac) cd)

Premises used: Ne.symm, Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
rw : (swap x y).cycleType + (swap z t).cycleType = {2, 2}
⊢ (swap x y * swap z t).cycleType = {2, 2}

Tactic:
rw [(disjoint_swap_swap h).cycleType_mul]

Premises used: Equiv.Perm.disjoint_swap_swap, Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
rw : HAdd.hAdd (α := Multiset ℕ) {2} {2} = {2, 2}
rw₁ : (swap z t).IsSwap
rw₂ : (swap x y).IsSwap
⊢ (swap x y).cycleType + (swap z t).cycleType = {2, 2}

Tactic:
rw [isSwap_iff_cycleType.mp ?_, isSwap_iff_cycleType.mp ?_]

Premises used: Iff.mp, Equiv.Perm.isSwap_iff_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ HAdd.hAdd (α := Multiset ℕ) {2} {2} = {2, 2}

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
rw : z ≠ t
⊢ (swap z t).IsSwap

Tactic:
rw [swap_isSwap_iff]

Premises used: Equiv.Perm.swap_isSwap_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ z ≠ t

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
rw : x ≠ y
⊢ (swap x y).IsSwap

Tactic:
rw [swap_isSwap_iff]

Premises used: Equiv.Perm.swap_isSwap_iff