mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x (σ x) ∈ H

Tactic:
]

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x (σ x) ∈ H
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ τ (τ x) ≠ τ x

Tactic:
]

Goal state after:
case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ τ (τ x) ≠ τ x
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ Equiv.refl α ∈ H

Tactic:
]

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ Equiv.refl α ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap ((σ ^ n) x) ((σ ^ (n + 1)) x) * swap x ((σ ^ n) x) * swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H

Tactic:
]

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap ((σ ^ n) x) ((σ ^ (n + 1)) x) * swap x ((σ ^ n) x) * swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((e.symm.trans (Equiv.trans f (swap x (f x)))) x✝)) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((e.symm.trans (Equiv.trans f (swap x (f x)))) x✝)) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
⊢ swap x y ∈ H

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
⊢ swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
hy : σ y ≠ y
⊢ swap x y ∈ H

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
hy : σ y ≠ y
⊢ swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
hy : σ y ≠ y
n : ℕ
hn : (σ ^ n) x = y
⊢ swap x ((σ ^ n) x) ∈ H

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
hy : σ y ≠ y
n : ℕ
hn : (σ ^ n) x = y
⊢ swap x ((σ ^ n) x) ∈ H
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((Equiv.trans f (swap x (f x))) (e.symm x✝))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((Equiv.trans f (swap x (f x))) (e.symm x✝))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g x = x ↔ g x = x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (if f⁻¹ ((Equiv.symm f) b) = x then (Equiv.symm f) x
    else if f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x then x else f⁻¹ ((Equiv.symm f) b)) ≠
    (Equiv.symm f) b

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (if f⁻¹ ((Equiv.symm f) b) = x then (Equiv.symm f) x
    else if f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x then x else f⁻¹ ((Equiv.symm f) b)) ≠
    (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ ∀ a ∈ (ofSubtype x).support, ∀ b ∈ σ.support, a ≠ b

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ ∀ a ∈ (ofSubtype x).support, ∀ b ∈ σ.support, a ≠ b
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H

Tactic:
]

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : (ofSubtype x) a ≠ a
hb : σ a ≠ a
⊢ False

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : (ofSubtype x) a ≠ a
hb : σ a ≠ a
⊢ False
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ H ⊓ K ≤ ⊥

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ H ⊓ K ≤ ⊥
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (((e.symm.trans f).trans e) x✝))

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (((e.symm.trans f).trans e) x✝))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
h : x = 1
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
h : x = 1
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ Equiv.refl α ∈ H

Tactic:
]

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : z = y
⊢ Equiv.refl α ∈ H
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e ((e.symm.trans f) x✝)))

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e ((e.symm.trans f) x✝)))
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap x y * swap x z * swap x y ∈ H

Tactic:
]

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap x y * swap x z * swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
⊢ {σ | σ.IsSwap} ⊆ ↑(closure {σ, swap x (σ x)})

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
⊢ {σ | σ.IsSwap} ⊆ ↑(closure {σ, swap x (σ x)})
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ∪ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
Set.union_subset_iff

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support ∧ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ (n + 1)) x = (Equiv.symm f) b

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ (n + 1)) x = (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support ∧ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
]

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support ∧ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ swap y z ∈ ↑(closure {σ, swap x (σ x)})

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ swap y z ∈ ↑(closure {σ, swap x (σ x)})
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h2 : σ.support = univ
x : α
m : ℕ
h1 : ((σ ^ n) ^ m).IsCycle
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
⊢ ((σ ^ n) ^ ↑m).IsCycle

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h2 : σ.support = univ
x : α
m : ℕ
h1 : ((σ ^ n) ^ m).IsCycle
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
⊢ ((σ ^ n) ^ ↑m).IsCycle
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : 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) x)}) ∧ {swap x ((σ ^ n) x)} ⊆ ↑(closure {σ, swap x ((σ ^ n) x)})

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : 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) x)}) ∧ {swap x ((σ ^ n) x)} ⊆ ↑(closure {σ, swap x ((σ ^ n) x)})
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
⊢ closure {σ, swap x ((σ ^ i) x)} = ⊤

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
⊢ closure {σ, swap x ((σ ^ i) x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
m : ℕ
hm : i = Fintype.card α * m
⊢ x = y

Tactic:
hm,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i m : ℕ
hi : (σ ^ (Fintype.card α * m)) x = y
hm : i = Fintype.card α * m
⊢ x = y