awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 : α)
⊢ σ ∈ l₁ ↔ σ ∈ l₂
have pos : (σ.IsCycle ∧
    ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l₁.prod : (a : α) → α) a : α)) ↔
  σ ∈ l₂
Tactic: rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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₂
⊢ σ ∈ l₁ ↔ σ ∈ l₂
have 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 : α)
Tactic: rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 : α)
⊢ σ ∈ l₁ ↔ σ ∈ l₂
have 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 : α)
Tactic: rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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₂
have h₁l₃ : ∀ (σ : Perm α), σ ∈ 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σ)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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₂
have pos : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ ∈ 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σ)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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₂
⊢ l₁ ~ l₂
have neg : ∀ (σ : Perm α) (hσ : ¬σ.IsCycle), σ ∈ 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σ)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have 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'
          sorry) =
      σ.truncCycleFactors),
  σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
Tactic: obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
have 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 := sorry : Finset (Perm α) })
    sorry σ.truncCycleFactors =
  l'.toFinset
Tactic: rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ σ.cycleFactorsFinset = l'.toFinset
have 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 := sorry : Finset (Perm α) })
    sorry
    (Trunc.mk
      (Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' sorry)) =
  l'.toFinset
Tactic: rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ σ.cycleFactorsFinset = l'.toFinset
have rw₂ : {
    val :=
      (↑(↑(Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l'
                sorry) :
            List (Perm α)) :
        Multiset (Perm α)),
    nodup := sorry : Finset (Perm α) } =
  l'.toFinset
Tactic: rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ σ.cycleFactorsFinset = l'.toFinset
have rw₃ : (↑(↑(Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' sorry) :
          List (Perm α)) :
      Multiset (Perm α)).toFinset =
  l'.toFinset
Tactic: rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ σ.cycleFactorsFinset = l'.toFinset
have rw₄ : (↑(Subtype.mk (p := fun (l : List (Perm α)) ↦ l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l) l' sorry) :
      List (Perm α)).toFinset =
  l'.toFinset
Tactic: rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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 ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have ht : σ.cycleFactorsFinset = l'.toFinset
Tactic: have ht : cycleFactorsFinset σ = l'.toFinset := by
    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have rw : l'.toFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ l'.toFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have mp : l'.toFinset = l.toFinset → (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 = σ
⊢ l'.toFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have mpr : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have hn' : l'.Nodup
Tactic: have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have hperm : l ~ l'
Tactic: have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 = σ
have mp : ∀ f ∈ l, f.IsCycle
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have mp₁ : List.Pairwise Disjoint l
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
have mp₂ : l.prod = σ
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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
have this : List.Pairwise Disjoint l ↔ List.Pairwise Disjoint l'
Tactic: have := List.Perm.pairwise_iff (@Disjoint.symmetric _) hperm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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'
⊢ l.prod = σ
have mp : List.Pairwise Commute l'
Tactic: rw [← hp', hperm.symm.prod_eq']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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'
have mp : ∀ {a b : Perm α}, a.Disjoint b → Commute a b
Tactic: refine hd'.imp ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
have mpr : l' ~ l
Tactic: refine List.toFinset_eq_of_perm _ _ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
have mpr : l'.prod = l.prod
Tactic: refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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.prod
have mpr₁ : σ = σ
Tactic: rw [hp, hp']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
s : Finset (Perm α)
⊢ σ.cycleFactorsFinset = s ↔
    (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s : Set (Perm α)).Pairwise Disjoint), s.noncommProd id ⋯ = σ
have 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 sorry = σ
Tactic: obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
⊢ Commute g1 g2
have inl : ∀ (h2 : g1 ∈ f.cycleFactorsFinset), Commute g1 g1
Tactic: rcases eq_or_ne g1 g2 with rfl | h
Cleared hypotheses: g2, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
inl : ∀ (h2 : g1 ∈ f.cycleFactorsFinset), Commute g1 g1
⊢ Commute g1 g2
have inr : ∀ (h : g1 ≠ g2), Commute g1 g2
Tactic: rcases eq_or_ne g1 g2 with rfl | h