awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
mp : a ∈ g.cycleType → 2 ≤ a
⊢ a ∈ m → 2 ≤ a

Tactic:
rw [← hg]
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
⊢ a ∈ g.cycleType → 2 ≤ a

Tactic:
Equiv.Perm.two_le_of_mem_cycleType

Premises used: Equiv.Perm.two_le_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
⊢ a ∈ g.cycleType → 2 ≤ a

Tactic:
exact Equiv.Perm.two_le_of_mem_cycleType

Premises used: Equiv.Perm.two_le_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
simp : m.sum ≤ Fintype.card α
⊢ m.toList.sum ≤ Fintype.card α

Tactic:
simp only [Multiset.sum_toList]

Premises used: Multiset.sum_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ m.sum ≤ Fintype.card α

Tactic:
hc
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ m.sum ≤ Fintype.card α

Tactic:
exact hc
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ m.toList.sum ≤ Fintype.card α

Tactic:
have hc' : m.toList.sum ≤ Fintype.card α := by
      simp only [Multiset.sum_toList]
      exact hc
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
mpr :
  ∀ (p : List (List α)) (hp_length : List.map List.length p = m.toList) (hp_nodup : ∀ s ∈ p, s.Nodup)
    (hp_disj : List.Pairwise List.Disjoint p), ∃ (g : Perm α), g.cycleType = m
⊢ ∃ (g : Perm α), g.cycleType = m

Tactic:
obtain ⟨p, hp_length, hp_nodup, hp_disj⟩ := List.exists_pw_disjoint_with_card hc'

Premises used: List.exists_pw_disjoint_with_card
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
h : cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m
⊢ ∃ (g : Perm α), g.cycleType = m

Tactic:
use List.prod (List.map (fun l => List.formPerm l) p)

Premises used: List.map, List.formPerm, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
apply : x.length ∈ m
⊢ 2 ≤ x.length

Tactic:
apply h2c x.length

Premises used: List.length
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
rw : ∃ a ∈ p, a.length = x.length
⊢ x.length ∈ m

Tactic:
rw [← Multiset.mem_toList, ← hp_length, List.mem_map]

Premises used: Multiset.mem_toList, List.mem_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, a.length = x.length

Tactic:
⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, a.length = x.length

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
⊢ ∀ x ∈ p, 2 ≤ x.length

Tactic:
have hp2 : ∀ x ∈ p, 2 ≤ x.length := by
      intro x hx
      apply h2c x.length
      rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
      exact ⟨x, hx, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) = m
h₁ : ∀ (σ : Perm α), Membership.mem (γ := List (Perm α)) (List.map (fun (l : List α) ↦ l.formPerm) p) σ → σ.IsCycle
h₂ : List.Pairwise (α := Perm α) Disjoint (List.map (fun (l : List α) ↦ l.formPerm) p)
⊢ cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m

Tactic:
rw [Equiv.Perm.cycleType_eq _ rfl]

Premises used: Equiv.Perm.cycleType_eq, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h :
  (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) =
    (↑m.toList : Multiset ℕ)
⊢ (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) = m

Tactic:
rw [← Multiset.coe_toList m]

Premises used: Multiset.coe_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p) = m.toList
⊢ (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) =
    (↑m.toList : Multiset ℕ)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p = m.toList
⊢ List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p) = m.toList

Tactic:
rw [List.map_map]

Premises used: List.map_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h :
  List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p =
    List.map List.length p
⊢ List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p = m.toList

Tactic:
rw [← hp_length]
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : ∀ a ∈ p, Function.comp (β := Perm α) (Finset.card ∘ support) (fun (l : List α) ↦ l.formPerm) a = a.length
⊢ List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p =
    List.map List.length p

Tactic:
apply List.map_congr_left

Premises used: List.map_congr_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
h : x.formPerm.support.card = x.length
⊢ Function.comp (β := Perm α) (Finset.card ∘ support) (fun (l : List α) ↦ l.formPerm) x = x.length

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
h : x.toFinset.card = x.length
h₁ : ∀ (x_1 : α), x ≠ [x_1]
⊢ x.formPerm.support.card = x.length

Tactic:
rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]

Premises used: List.support_formPerm_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
h h₁ : x.length = x.length
⊢ x.toFinset.card = x.length

Tactic:
rw [List.toFinset_card_of_nodup (hp_nodup x hx)]

Premises used: List.toFinset_card_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ ∀ (σ : Perm α), Membership.mem (γ := List (Perm α)) (List.map (fun (l : List α) ↦ l.formPerm) p) σ → σ.IsCycle

Tactic:
simpa using fun a b ↦ List.isCycle_formPerm (hp_nodup a b) (hp2 a b)

Premises used: List.isCycle_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : List.Pairwise (fun (a b : List α) ↦ a.formPerm.Disjoint b.formPerm) p
⊢ List.Pairwise (α := Perm α) Disjoint (List.map (fun (l : List α) ↦ l.formPerm) p)

Tactic:
rw [List.pairwise_map]

Premises used: List.pairwise_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
apply : ∀ {a b : List α}, a ∈ p → b ∈ p → a.Disjoint b → a.formPerm.Disjoint b.formPerm
⊢ List.Pairwise (fun (a b : List α) ↦ a.formPerm.Disjoint b.formPerm) p

Tactic:
apply List.Pairwise.imp_of_mem _ hp_disj

Premises used: List.Pairwise.imp_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab rw : a.Disjoint b
⊢ a.formPerm.Disjoint b.formPerm

Tactic:
rw [List.formPerm_disjoint_iff (hp_nodup a ha) (hp_nodup b hb) (hp2 a ha) (hp2 b hb)]

Premises used: List.formPerm_disjoint_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : a.Disjoint b
⊢ a.Disjoint b

Tactic:
hab
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : a.Disjoint b
⊢ a.Disjoint b

Tactic:
exact hab
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType = Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val

Tactic:
rfl

Premises used: Equiv.Perm.cycleType, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s : Set (Perm α)).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
e_s : σ.cycleFactorsFinset = s
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s : Set (Perm α)).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
e_s : (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s : Set (Perm α)).Pairwise Disjoint), s.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s

Tactic:
rw [cycleFactorsFinset_eq_finset]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_finset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s : Set (Perm α)).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s : Set (Perm α)).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
⟨h1, h2, h0⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s : Set (Perm α)).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s : Set (Perm α)).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
exact ⟨h1, h2, h0⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
⊢ l.Nodup

Tactic:
have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
rw : Multiset.map (Finset.card ∘ support) l.toFinset.val = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)
h1₁ : ∀ f ∈ l.toFinset, f.IsCycle
h2₁ : (↑l.toFinset : Set (Perm α)).Pairwise Disjoint
h0₁ : l.toFinset.noncommProd id ⋯ = σ
⊢ σ.cycleType = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)

Tactic:
rw [cycleType_eq' l.toFinset]

Premises used: Equiv.Perm.cycleType_eq', List.toFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ Multiset.map (Finset.card ∘ support) l.toFinset.val = (↑(List.map (Finset.card ∘ support) l) : Multiset ℕ)

Tactic:
simp [List.dedup_eq_self.mpr hl, Function.comp_def]

Premises used: Iff.mpr, List.dedup_eq_self, Function.comp_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ ∀ f ∈ l.toFinset, f.IsCycle

Tactic:
simpa using h1
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ (↑l.toFinset : Set (Perm α)).Pairwise Disjoint

Tactic:
simpa [hl] using h2
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ

Tactic:
simp [hl, h0]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
rw :
  (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card.{u_1} { c : ↥σ.cycleFactorsFinset // #(↑c : Perm α).support = n }
⊢ Multiset.count n σ.cycleType = Fintype.card.{u_1} { c : ↥σ.cycleFactorsFinset // #(↑c : Perm α).support = n }

Tactic:
rw [cycleType, Multiset.count_eq_card_filter_eq]

Premises used: Equiv.Perm.cycleType, Multiset.count_eq_card_filter_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
rw :
  (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({x ∈ σ.cycleFactorsFinset |
        ∃ (h : x ∈ σ.cycleFactorsFinset),
          #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ σ.cycleFactorsFinset) x h) : Perm α).support = n})
⊢ (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card.{u_1} { c : ↥σ.cycleFactorsFinset // #(↑c : Perm α).support = n }

Tactic:
rw [Fintype.subtype_card, Finset.univ_eq_attach, Finset.filter_attach',
    Finset.card_map, Finset.card_attach]

Premises used: Finset.card_map, Fintype.subtype_card, Finset.card_attach, Finset.univ_eq_attach, Finset.filter_attach'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
simp :
  (Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val).card =
    (Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
        σ.cycleFactorsFinset.val).card
⊢ (Multiset.filter (fun (x : ℕ) ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({x ∈ σ.cycleFactorsFinset |
        ∃ (h : x ∈ σ.cycleFactorsFinset),
          #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ σ.cycleFactorsFinset) x h) : Perm α).support = n})

Tactic:
simp only [Function.comp_apply, Finset.card, Finset.filter_val,
    Multiset.filter_map, Multiset.card_map]

Premises used: Finset.filter_val, Multiset.filter_map, Finset.card, Function.comp_apply, Multiset.card_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
e_a :
  Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val =
    Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
      σ.cycleFactorsFinset.val
⊢ (Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val).card =
    (Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
        σ.cycleFactorsFinset.val).card

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
e_a : ∀ x ∈ σ.cycleFactorsFinset.val, n = x.support.val.card ↔ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n
⊢ Multiset.filter (fun (x : Perm α) ↦ n = x.support.val.card) σ.cycleFactorsFinset.val =
    Multiset.filter (fun (x : Perm α) ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n)
      σ.cycleFactorsFinset.val

Tactic:
apply Multiset.filter_congr

Premises used: Multiset.filter_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
d : Perm α
h : d ∈ σ.cycleFactorsFinset.val
⊢ n = d.support.val.card ↔ ∃ (_ : d ∈ σ.cycleFactorsFinset), d.support.val.card = n

Tactic:
simp only [eq_comm, Finset.mem_val.mp h, exists_const]

Premises used: Eq.mp, eq_comm, exists_const, Finset.mem_val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType = 0 ↔ σ = 1

Tactic:
simp [cycleType_def, cycleFactorsFinset_eq_empty_iff]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_empty_iff, Equiv.Perm.cycleType_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ cycleType.{u_1} (α := α) 1 = 0

Tactic:
cycleType_eq_zero.2 rfl

Premises used: Iff.mpr, Equiv.Perm.cycleType_eq_zero, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType = 0 ↔ σ = 1
rw₁ rw₂ : σ = 1 ↔ σ = 1
⊢ σ.cycleType.card = 0 ↔ σ = 1

Tactic:
rw [card_eq_zero, cycleType_eq_zero]

Premises used: Multiset.card_eq_zero, Equiv.Perm.cycleType_eq_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ 0 < σ.cycleType.card ↔ σ ≠ 1

Tactic:
pos_iff_ne_zero.trans card_cycleType_eq_zero.not

Premises used: Iff.not, Equiv.Perm.card_cycleType_eq_zero, Iff.trans, pos_iff_ne_zero