awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
intro :
  ∀ (val : Fintype α),
    σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
intro₁ :
  ∀ (val : Fintype α),
    σ ∈ l → ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
intro₂ intro₃ :
  ∀ (val : Fintype α),
    (∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)) → σ ∈ l
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)

Premises used: Equiv.Perm.mem_support, id, nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
⊢ l₁ ~ l₂

Tactic:
(List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
        fun σ => ?_

Premises used: Iff.mpr, List.perm_ext_iff_of_nodup, Equiv.Perm.nodup_of_pairwise_disjoint_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
h₁l₃ : ∀ (σ : Perm α), σ ∈ l₁ ↔ σ ∈ l₂
⊢ l₁ ~ l₂

Tactic:
refine
      (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
        fun σ => ?_

Premises used: Iff.mpr, List.perm_ext_iff_of_nodup, Equiv.Perm.nodup_of_pairwise_disjoint_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
pos : ∀ (hσ : σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
neg : ∀ (hσ : ¬σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
by_cases hσ : σ.IsCycle

Premises used: Equiv.Perm.IsCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
⊢ ∃ (x : α), ¬Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
obtain _ := not_forall.mp (mt ext hσ.ne_one)

Premises used: mt, Equiv.Perm.IsCycle.ne_one, Iff.mp, Classical.not_forall, Equiv.Perm.ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
h : ∃ (x : α), ¬Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
pos :
  (σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l₁.prod : (a : α) → α) a : α)) ↔
    σ ∈ l₂
pos₁ :
  (σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l₁.prod : (a : α) → α) a : α)) ↔
    σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l₂.prod : (a : α) → α) a : α)
pos₂ pos₃ :
  (σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l₂.prod : (a : α) → α) a : α)) ↔
    σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l₂.prod : (a : α) → α) a : α)
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]

Premises used: Equiv.Perm.mem_list_cycles_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)

Premises used: mt, iff_of_false
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)

Premises used: mt, iff_of_false
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
h₁l₃ : ∀ (σ : Perm α), σ ∈ l₁ ↔ σ ∈ l₂
pos : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
neg neg₁ : ∀ (σ : Perm α) (hσ : ¬σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
⊢ l₁ ~ l₂

Tactic:
classical
    refine
      (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
        fun σ => ?_
    by_cases hσ : σ.IsCycle
    · obtain _ := not_forall.mp (mt ext hσ.ne_one)
      rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
    · exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)

Premises used: Iff.mpr, Equiv.Perm.mem_list_cycles_iff, List.perm_ext_iff_of_nodup, Equiv.Perm.nodup_of_pairwise_disjoint_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
obtain :
  ∀ (l' : List (Perm α)) (hp' : l'.prod = σ) (hc' : ∀ g ∈ l', g.IsCycle) (hd' : List.Pairwise Disjoint l')
    (hl :
      Trunc.mk
          (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l'
            ⋯) =
        σ.truncCycleFactors),
    σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors

Premises used: Trunc.exists_rep, Equiv.Perm.truncCycleFactors
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
rw :
  Trunc.lift
      (fun (l : { l : List (Perm α) // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l }) ↦
        { val := (↑(↑l : List (Perm α)) : Multiset (Perm α)), nodup := ⋯ : Finset (Perm α) })
      ⋯ σ.truncCycleFactors =
    l'.toFinset
rw₁ :
  Trunc.lift
      (fun (l : { l : List (Perm α) // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l }) ↦
        { val := (↑(↑l : List (Perm α)) : Multiset (Perm α)), nodup := ⋯ : Finset (Perm α) })
      ⋯
      (Trunc.mk
        (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l'
          ⋯)) =
    l'.toFinset
rw₂ :
  {
      val :=
        (↑(↑(Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l'
                  ⋯) :
              List (Perm α)) :
          Multiset (Perm α)),
      nodup := ⋯ : Finset (Perm α) } =
    l'.toFinset
rw₃ :
  (↑(↑(Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) :
            List (Perm α)) :
        Multiset (Perm α)).toFinset =
    l'.toFinset
rw₄ rw₅ :
  (↑(Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) :
        List (Perm α)).toFinset =
    l'.toFinset
⊢ σ.cycleFactorsFinset = l'.toFinset

Tactic:
rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]

Premises used: Equiv.Perm.cycleFactorsFinset, Trunc.lift_mk, List.toFinset_coe, Multiset.toFinset_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
⊢ σ.cycleFactorsFinset = l'.toFinset

Tactic:
have ht : cycleFactorsFinset σ = l'.toFinset := by
    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
rw : l'.toFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
rw [ht]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
mp : l'.toFinset = l.toFinset → (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
mpr : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset
⊢ l'.toFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
⊢ l'.Nodup

Tactic:
have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
⊢ l ~ l'

Tactic:
have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
mp : ∀ f ∈ l, f.IsCycle
mp₁ : List.Pairwise Disjoint l
mp₂ : l.prod = σ
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ ∀ f ∈ l, f.IsCycle

Tactic:
fun _ h => hc' _ (hperm.subset h)

Premises used: List.Perm.subset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ ∀ f ∈ l, f.IsCycle

Tactic:
exact fun _ h => hc' _ (hperm.subset h)

Premises used: List.Perm.subset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ List.Pairwise Disjoint l ↔ List.Pairwise Disjoint l'

Tactic:
have := List.Perm.pairwise_iff (@Disjoint.symmetric _) hperm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
this : List.Pairwise Disjoint l ↔ List.Pairwise Disjoint l'
mp mp₁ mp₂ mp₃ : List.Pairwise Disjoint l'
⊢ List.Pairwise Disjoint l

Tactic:
rwa [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
mp : List.Pairwise Commute l'
⊢ l.prod = σ

Tactic:
rw [← hp', hperm.symm.prod_eq']

Premises used: List.Perm.symm, List.Perm.prod_eq'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ List.Pairwise Commute l'

Tactic:
hd'.imp ?_

Premises used: List.Pairwise.imp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
mp : ∀ {a b : Perm α}, a.Disjoint b → Commute a b
⊢ List.Pairwise Commute l'

Tactic:
refine hd'.imp ?_

Premises used: List.Pairwise.imp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
a b : Perm α
⊢ a.Disjoint b → Commute a b

Tactic:
Disjoint.commute

Premises used: Equiv.Perm.Disjoint.commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ ∀ {a b : Perm α}, a.Disjoint b → Commute a b

Tactic:
exact Disjoint.commute

Premises used: Equiv.Perm.Disjoint.commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l'.toFinset = l.toFinset

Tactic:
List.toFinset_eq_of_perm _ _ ?_

Premises used: List.toFinset_eq_of_perm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
mpr : l' ~ l
⊢ l'.toFinset = l.toFinset

Tactic:
refine List.toFinset_eq_of_perm _ _ ?_

Premises used: List.toFinset_eq_of_perm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l' ~ l

Tactic:
list_cycles_perm_list_cycles ?_ hc' hc hd' hd

Premises used: Equiv.Perm.list_cycles_perm_list_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
mpr : l'.prod = l.prod
⊢ l' ~ l

Tactic:
refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd

Premises used: Equiv.Perm.list_cycles_perm_list_cycles
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' ⋯) =
    σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
mpr : l'.prod = σ
mpr₁ mpr₂ : σ = σ
⊢ l'.prod = l.prod

Tactic:
rw [hp, hp']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
s : Finset (Perm α)
obtain :
  ∀ (l : List (Perm α)) (hl : l.Nodup),
    σ.cycleFactorsFinset = l.toFinset ↔
      (∀ f ∈ l.toFinset, f.IsCycle) ∧
        ∃ (h : (↑l.toFinset : Set (Perm α)).Pairwise Disjoint), l.toFinset.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s ↔
    (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s : Set (Perm α)).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq

Premises used: Finset.exists_list_nodup_eq, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hl : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔
    (∀ f ∈ l.toFinset, f.IsCycle) ∧
      ∃ (h : (↑l.toFinset : Set (Perm α)).Pairwise Disjoint), l.toFinset.noncommProd id ⋯ = σ

Tactic:
simp [cycleFactorsFinset_eq_list_toFinset, hl]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_list_toFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ (↑f.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint

Tactic:
(cycleFactorsFinset_eq_finset.mp rfl).2.choose

Premises used: Equiv.Perm.cycleFactorsFinset_eq_finset, And.right, Iff.mp, Exists.choose, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ (↑f.cycleFactorsFinset : Set (Perm α)).Pairwise Commute

Tactic:
(cycleFactorsFinset_pairwise_disjoint _).mono' fun _ _ => Disjoint.commute

Premises used: Equiv.Perm.Disjoint.commute, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Set.Pairwise.mono'