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

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

pp: case succ
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ ∃ i_1, 0 < i_1 ∧ i_1 ≤ orderOf f ∧ (f ^ i_1) x = (f ^ (i + 1)) x

Tactic:
·

Goal state after:
case zero
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ ∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = (f ^ 0) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
·

Goal state after:
case succ
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ ∃ i_1, 0 < i_1 ∧ i_1 ≤ orderOf f ∧ (f ^ i_1) x = (f ^ (i + 1)) x
Module: Mathlib.GroupTheory.Perm.List

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

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

pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1

Tactic:
·

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ [].formPerm = l'.formPerm ↔ [] ~r l' ∨ [].length ≤ 1 ∧ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inl
n : ℕ
a₂ : Fin (n + 2)
ha₂ : ⟨0, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < 0
⊢ (if (swap 0 1) 0 ≤ (swap 0 1) a₂ then -1 else 1) = 1

pp: case inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
·

Goal state after:
case inl
n : ℕ
a₂ : Fin (n + 2)
ha₂ : ⟨0, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < 0
⊢ (if (swap 0 1) 0 ≤ (swap 0 1) a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr
α : 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
⊢ ↑((Set.union hd2'').symm
        (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inr ⟨↑⟨(σ * τ) x, ⋯⟩, ?intro.refine_2.inr.ha✝⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm
          (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inr ⟨↑⟨x, ⋯⟩, ?intro.refine_2.inr.ha⟩)))

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, ⋯⟩ ∈ ↑τ.support

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, ⋯⟩ ∈ ↑τ.support

Tactic:
·

Goal state after:
case intro.refine_2.inr
α : 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
⊢ ↑((Set.union hd2'').symm
        (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inr ⟨↑⟨(σ * τ) x, ⋯⟩, ?intro.refine_2.inr.ha✝⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm
          (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inr ⟨↑⟨x, ⋯⟩, ?intro.refine_2.inr.ha⟩)))
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil.inl
α : Type u_1
inst✝ : DecidableEq α
hl hl' : [].Nodup
⊢ [].length ≤ 1

pp: case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
·

Goal state after:
case nil.inl
α : Type u_1
inst✝ : DecidableEq α
hl hl' : [].Nodup
⊢ [].length ≤ 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
·

Goal state after:
case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ⟨a₁, 0⟩ ∉ {⟨1, 0⟩}
ha₁ : 0 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1

pp: case inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
·

Goal state after:
case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ⟨a₁, 0⟩ ∉ {⟨1, 0⟩}
ha₁ : 0 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.List

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

pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_1
α : 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
⊢ (g.extendDomain f) ↑(f a) ≠ ↑(f a)

pp: case refine_2
α : 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
⊢ (g.extendDomain f).SameCycle (↑(f a)) b

Tactic:
·

Goal state after:
case refine_1
α : 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
⊢ (g.extendDomain f) ↑(f a) ≠ ↑(f a)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_2
α : 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
h : (f * σ * f⁻¹) (g (τ x)) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))

pp: case intro.refine_2.inr.refine_1
α : 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
⊢ ¬(g * τ * g⁻¹) (g (τ x)) = g (τ x)

Tactic:
·

Goal state after:
case intro.refine_2.inr.refine_2
α : 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
h : (f * σ * f⁻¹) (g (τ x)) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.nil.inl
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : [x] ~r l'
⊢ l'.length ≤ 1

pp: case cons.nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
·

Goal state after:
case cons.nil.inl
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : [x] ~r l'
⊢ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
·

Goal state after:
case cons.nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
·

Goal state after:
case inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
·

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.List

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

pp: case cons.cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' : α
hl' : [x'].Nodup
⊢ (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1

pp: case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Tactic:
·

Goal state after:
case cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
hl' : [].Nodup
⊢ (x :: y :: l).formPerm = [].formPerm ↔ x :: y :: l ~r [] ∨ (x :: y :: l).length ≤ 1 ∧ [].length ≤ 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
ha₂ : ⟨a₁, 1⟩ ∉ {⟨1, 0⟩}
ha₁ : 1 < a₁
H' : 0 < 1
le : 1 ≤ 1
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 1 then -1 else 1) = 1

pp: case inr.inr.inr
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₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
·

Goal state after:
case inr.inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
ha₂ : ⟨a₁, 1⟩ ∉ {⟨1, 0⟩}
ha₁ : 1 < a₁
H' : 0 < 1
le : 1 ≤ 1
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 1 then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.List

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

pp: case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Tactic:
·

Goal state after:
case cons.cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' : α
hl' : [x'].Nodup
⊢ (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
·

Goal state after:
case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inr.inr
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₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
·

Goal state after:
case inr.inr.inr
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₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.List

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

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

pp: case mpr
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ a ≠ b → (swap a b).IsSwap

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).IsSwap → a ≠ b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ a ≠ b → (swap a b).IsSwap
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.Sign

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

pp: case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

pp: case succ.succ
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
·

Goal state after:
case zero
hn : 2 ≤ 0
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_1
α : 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
⊢ ¬(g * τ * g⁻¹) (g (τ x)) = g (τ x)

Tactic:
·

Goal state after:
case intro.refine_2.inr.refine_1
α : 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
⊢ ¬(g * τ * g⁻¹) (g (τ x)) = g (τ x)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

pp: case succ.succ
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
·

Goal state after:
case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
·

Goal state after:
case succ.succ
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

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

Tactic:
·

Goal state after:
case left
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
⊢ Injective fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm ^ l.length) x = 1 x

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm ^ l.length) x = 1 x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : ¬σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y

Tactic:
·

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : ¬σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y

Tactic:
·

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : ¬σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : ¬σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y

Tactic:
obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
i : ℤ
hy : ¬σ ((σ ^ i) (Classical.choose hσ)) = (σ ^ i) (Classical.choose hσ)
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ ((σ ^ i) (Classical.choose hσ)) = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ ((σ ^ i) (Classical.choose hσ))
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
·

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