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

Goal state before:
pp: case inr.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
try rw [hστ, hτυ, swap_mul_self_mul]

Goal state after:
case inr.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : ((Equiv.symm g) x :: l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f ((Equiv.symm g) x) = (Equiv.symm g) x
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap ((Equiv.symm g) x) b * f) (permsOfList l)) l
hx' : f ∈ List.map (fun f ↦ Equiv.swap ((Equiv.symm g) x) x * f) (permsOfList l)
hg : g ∈ permsOfList l ∧ Equiv.swap ((Equiv.symm g) x) x * g = f
hxa : x ≠ (Equiv.symm g) x
⊢ g ((Equiv.symm g) x) ≠ (Equiv.symm g) x

Tactic:
by

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

Goal state before:
pp: case inr.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
try rw [hστ, hτυ, swap_mul_self_mul]

Goal state after:
case inr.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ υ = υ ∨ υ = swap i j * υ
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
⊢ (permsOfList (a :: l)).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
a b : List α
hab : a ≈ b
ha : Multiset.Nodup ⟦a⟧
hb : Multiset.Nodup ⟦b⟧
x✝ : ha ≍ hb
⊢ ∀ (a_1 : Equiv.Perm α), a_1 ∈ { val := ↑(permsOfList a), nodup := ⋯ } ↔ a_1 ∈ { val := ↑(permsOfList b), nodup := ⋯ }

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ ∨ σ = swap i j * τ
hτυ : τ = υ ∨ τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ [].prod x = f x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
⊢ ∀ g ∈ [], g.IsSwap

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (s : Finset α), #(permsOfFinset s) = (#s)!

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h✝ : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = f x
y : α
hy : f y ≠ y
h : y = x
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Fintype α
⊢ ∀ (x : Equiv.Perm α), x ∈ permsOfFinset univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (a a' : α ≃ β),
    ∀ b ∈ if h : ∀ (a_1 b : α), a (a_1 * b) = a a_1 * a b then some { toEquiv := a, map_mul' := h } else none,
      (b ∈ if h : ∀ (a b : α), a' (a * b) = a' a * a' b then some { toEquiv := a', map_mul' := h } else none) → a = a'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
me : α ≃* β
⊢ (if h : ∀ (a b : α), me.toEquiv (a * b) = me.toEquiv a * me.toEquiv b then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ (swap x (f x) :: ↑m).prod = f

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α), (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
⊢ g ∈ g :: l

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
⊢ motive f

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
⊢ Submonoid.closure {σ | σ.IsSwap} = ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ) = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ w ≠ y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd < a.fst

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ signAux 1 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
⊢ Set.InjOn f.signBijAux ↑(finPairsLT n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : (Equiv.symm f) a₂ < (Equiv.symm f) a₁
⊢ f.signBijAux ⟨(Equiv.symm f) a₁, (Equiv.symm f) a₂⟩ = ⟨a₁, a₂⟩

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬(Equiv.symm f) a₂ < (Equiv.symm f) a₁
h : (Equiv.symm f) a₁ = (Equiv.symm f) a₂
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬(Equiv.symm f) a₂ < (Equiv.symm f) a₁
⊢ f.signBijAux ⟨(Equiv.symm f) a₂, (Equiv.symm f) a₁⟩ = ⟨a₁, a₂⟩

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
⊢ f.signBijAux ⟨a₁, a₂⟩ ∈ finPairsLT n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
h : x = y
f : Perm α
⊢ f.SameCycle x y

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) =
    if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ (-i)) y = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y z : α
x✝¹ : f.SameCycle x y
x✝ : f.SameCycle y z
i : ℤ
hi : (f ^ i) x = y
j : ℤ
hj : (f ^ j) y = z
⊢ (f ^ (j + i)) x = z

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
⊢ SameCycle 1 x y ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ (∃ b, (f⁻¹ ^ (Equiv.symm (Equiv.neg ℤ)) b) x = y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x y : α
i : ℤ
⊢ ((g * f * g⁻¹) ^ i) x = y ↔ (f ^ i) (g⁻¹ x) = g⁻¹ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ x :: y :: l ~r x' :: y' :: l'

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x y : α
⊢ f.SameCycle x y → (g * f * g⁻¹).SameCycle (g x) (g y)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ f y = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ (∃ b, (f ^ (Equiv.symm (Equiv.addRight 1)) b) (f x) = y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x (f y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle ((Equiv.symm f) x) y ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x ((Equiv.symm f) y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ (∃ b, (f ^ (Equiv.symm (Equiv.addRight n)) b) ((f ^ n) x) = y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℕ
x✝ : (f ^ n).SameCycle x y
m : ℤ
h : ((f ^ n) ^ m) x = y
⊢ (f ^ (↑n * m)) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
x✝ : (f ^ n).SameCycle x y
m : ℤ
h : ((f ^ n) ^ m) x = y
⊢ (f ^ (n * m)) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
p : α → Prop
h : ∀ (x : α), p (f x) ↔ p x
x y : { x // p x }
n : ℤ
⊢ (f.subtypePerm h ^ n) x = y ↔ (f ^ n) ↑x = ↑y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x = x ↔ l.length ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ (g.extendDomain f ^ n) ↑(f x) = ↑(f y) ↔ (g ^ n) x = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x ≠ x ↔ 2 ≤ l.length

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (f ^ k) x = (f ^ k) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
⊢ f.SameCycle x y → ∃ i < orderOf f, (f ^ i) x = y

Tactic:
by

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

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
⊢ (f * g).signAux = f.signAux * g.signAux

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝ : (_ : Fin (n + 2)) × Fin (n + 2)
x₁ x₂ : Fin (n + 2)
⊢ ⟨x₁, x₂⟩ ∈ {⟨1, 0⟩} → ⟨x₁, x₂⟩ ∈ finPairsLT (n + 2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm = 1 ↔ l.length ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ (f ^ i.succ) x = (f ^ (i + 1)) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, (f ^ ↑i) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, (f ^ i) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
h : f.IsCycle
hf : f = 1
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
this : l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1
⊢ [].formPerm = l'.formPerm ↔ [] ~r l' ∨ [].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a)) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹) (g x) ≠ g x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
⊢ f.IsCycle → (g * f * g⁻¹).IsCycle

Tactic:
by

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

Goal state before:
pp: n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ (swap 0 1) 0 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
this : l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
⊢ b = ↑(f (f.symm ⟨b, ⋯⟩))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ g.IsCycle → (g.extendDomain f).IsCycle

Tactic:
by

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

Goal state before:
pp: n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ (swap 0 1) 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
⊢ ∃ i, (f ^ i) x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ (swap x y) y ≠ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
⊢ l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (swap x y ^ 1) y = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableEq α
⊢ f.IsSwap → f.IsCycle

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ 0 < 2

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).IsSwap ↔ a ≠ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
τ : ↑↑(Subgroup.zpowers σ)
⊢ ↑τ (Classical.choose hσ) ∈ σ.support

Tactic:
by

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

Goal state before:
pp: x y : Fin 0
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
by

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

Goal state before:
pp: x y : Fin 1
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ x ∉ {x | (l.formPerm ^ l.length) x ≠ x}

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ ⟨0, ⋯⟩ ≠ ⟨1, ⋯⟩

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm ^ l.length = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f

Tactic:
by

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
⊢ closure {σ | σ.IsCycle} = ⊤

Tactic:
by

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
⊢ ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
⊢ Bijective fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ orderOf f = #f.support

Tactic:
by

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
y : α
hy : f y ≠ y
h : y = x
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : 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
⊢ (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : 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
⊢ f ((f ^ n) (f x)) = f ((Equiv.symm f) b)

Tactic:
by

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
⊢ ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H

Tactic:
by

Goal state after: