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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, σ' a = τ a
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ {(Finset.card ∘ support) σ'} = {#σ'.support}

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, σ' a = τ a
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ {(Finset.card ∘ support) σ'} = {#σ'.support}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ g * g.cycleOf x = g.cycleOf x * g

Tactic:
]

Goal state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ g * g.cycleOf x = g.cycleOf x * g
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this✝ : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
this : (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j
⊢ ↑⟨(castLEEmb ⋯) 0, ⋯⟩ = 0

Tactic:
]

Goal state after:
case pos
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this✝ : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
this : (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j
⊢ ↑⟨(castLEEmb ⋯) 0, ⋯⟩ = 0
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(if i = j then 0 else i + 1) = if i = j then 0 else ↑i + 1

Tactic:
]

Goal state after:
case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(if i = j then 0 else i + 1) = if i = j then 0 else ↑i + 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i < j
⊢ i + 1 = i + 1

Tactic:
]

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

Goal state before:
pp: case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ π.cycleType = π.cycleType

pp: case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset

Tactic:
]

Goal state after:
case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
h : i < j
⊢ ↑i + 1 = ↑i + 1

Tactic:
]

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i = j
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset.val

Tactic:
]

Goal state after:
case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset.val
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑j = ↑j

Tactic:
]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (if i = last n then 0 else ↑i + 1) = if i = last n then 0 else ↑i + 1

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧ (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (g.cycleOf x :: m)

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧ (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (g.cycleOf x :: m)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ ↑j + 1 = ↑j + 1

Tactic:
]

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

Goal state before:
pp: case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ = j.succ

pp: case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ 0

pp: case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ i.succ

pp: case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ

Tactic:
]

Goal state after:
case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ 0

case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ i.succ

case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ

Tactic:
]

Goal state after:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ 0 = 0

pp: case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ castSucc 0 < i.succ

Tactic:
]

Goal state after:
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ castSucc 0 < i.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ 0 < i.succ

Tactic:
]

Goal state after:
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ 0 < i.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ σ.cycleType = σ.cycleType

Tactic:
]

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ = j.succ

pp: case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ 0

pp: case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ i.succ

pp: case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc

Tactic:
]

Goal state after:
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ 0

case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ i.succ

case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ : Perm α
hσ : σ.IsCycle
⊢ {#σ.support} = {#σ.support}

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.succ = j.succ

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.succ = j.succ

Tactic:
]

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

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : (σ.extendDomain f).cycleType = σ.cycleType
hτ : (τ.extendDomain f).cycleType = τ.cycleType
⊢ σ.cycleType + τ.cycleType = σ.cycleType + τ.cycleType

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ g.SameCycle x y

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ g.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
α : Type u_1
a : α
x : Fin n → α
p j : Fin (n + 1)
⊢ p.insertNth a x j = p.insertNth a x j

Tactic:
]

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

Goal state before:
pp: case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
]

Goal state after:
case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x (g y)
⊢ ¬(m.erase g').prod y = y

Tactic:
]

Goal state after:
case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x (g y)
⊢ ¬(m.erase g').prod y = y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c

Tactic:
]

Goal state after:
case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
⊢ {↑2 + 1} = {3}

Tactic:
]

Goal state after:
n : ℕ
⊢ {↑2 + 1} = {3}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = l.prod

Tactic:
]

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

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))) = k

pp: case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ (j - i).castLT ⋯ < subNat (↑i) (Fin.cast ⋯ k) ⋯

Tactic:
]

Goal state after:
case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))) = k

case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ (j - i).castLT ⋯ < subNat (↑i) (Fin.cast ⋯ k) ⋯
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ x ∈ l.prod.support

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ x ∈ l.prod.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
⊢ {#c.support} = {#c.support}

Tactic:
]

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ σ x ≠ x

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ σ x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : #c.support ∈ (c * g').cycleType
g'1 : g' ≠ 1
⊢ #c.support + #g'.support ≤ #c.support + #g'.support

Tactic:
]

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

Goal state before:
pp: case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
⊢ σ ∈ l

Tactic:
]

Goal state after:
case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
⊢ σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : σ a ≠ a
⊢ σ ∈ l

Tactic:
rw [← mem_support] at ha

Goal state after:
case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
⊢ σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, τ x = l.prod x
x : α
hx : x ∈ σ.support ∩ τ.support
⊢ l.prod x = l.prod x

Tactic:
]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-1) ^ σ.cycleType.card = (-1) ^ σ.cycleType.card

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ 1 = 1

Tactic:
]

Goal state after: