case intro.mk.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
case intro.mk.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
case intro.mk.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
have ht : cycleFactorsFinset σ = l'.toFinset := by
  rw [cycleFactorsFinset, ← hl, Trunc.lift_mk]
case intro.mk.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ List.toFinset l' = List.toFinset l ↔ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
case intro.mk.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
rw [ht]
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ List.toFinset l' = List.toFinset l → (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ

case intro.mk.intro.intro.mpr
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ → List.toFinset l' = List.toFinset l
case intro.mk.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ List.toFinset l' = List.toFinset l ↔ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
constructor
no goals
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
⊢ cycleFactorsFinset σ = List.toFinset l'
rw [cycleFactorsFinset, ← hl, Trunc.lift_mk]
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ List.toFinset l' = List.toFinset l → (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
intro h
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
case intro.mk.intro.intro.mp.refine'_1
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ ∀ (f : Perm α), f ∈ l → IsCycle f

case intro.mk.intro.intro.mp.refine'_2
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ List.Pairwise Disjoint l

case intro.mk.intro.intro.mp.refine'_3
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ List.prod l = σ
case intro.mk.intro.intro.mp
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ
refine' ⟨_, _, _⟩
no goals
case intro.mk.intro.intro.mp.refine'_1
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ ∀ (f : Perm α), f ∈ l → IsCycle f
exact fun _ h => hc' _ (hperm.subset h)
no goals
case intro.mk.intro.intro.mp.refine'_2
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ List.Pairwise Disjoint l
rwa [List.Perm.pairwise_iff Disjoint.symmetric hperm]
case intro.mk.intro.intro.mp.refine'_3
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ List.Pairwise _root_.Commute l'
case intro.mk.intro.intro.mp.refine'_3
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ List.prod l = σ
rw [← hp', hperm.symm.prod_eq']
case intro.mk.intro.intro.mp.refine'_3
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ ∀ {a b : Perm α}, Disjoint a b → _root_.Commute a b
case intro.mk.intro.intro.mp.refine'_3
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ List.Pairwise _root_.Commute l'
refine' hd'.imp _
no goals
case intro.mk.intro.intro.mp.refine'_3
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
h : List.toFinset l' = List.toFinset l
hn' : List.Nodup l'
hperm : l ~ l'
⊢ ∀ {a b : Perm α}, Disjoint a b → _root_.Commute a b
exact Disjoint.commute
case intro.mk.intro.intro.mpr.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
hc : ∀ (f : Perm α), f ∈ l → IsCycle f
hd : List.Pairwise Disjoint l
hp : List.prod l = σ
⊢ List.toFinset l' = List.toFinset l
case intro.mk.intro.intro.mpr
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
⊢ (∀ (f : Perm α), f ∈ l → IsCycle f) ∧ List.Pairwise Disjoint l ∧ List.prod l = σ → List.toFinset l' = List.toFinset l
rintro ⟨hc, hd, hp⟩
case intro.mk.intro.intro.mpr.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
hc : ∀ (f : Perm α), f ∈ l → IsCycle f
hd : List.Pairwise Disjoint l
hp : List.prod l = σ
⊢ l' ~ l
case intro.mk.intro.intro.mpr.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
hc : ∀ (f : Perm α), f ∈ l → IsCycle f
hd : List.Pairwise Disjoint l
hp : List.prod l = σ
⊢ List.toFinset l' = List.toFinset l
refine' List.toFinset_eq_of_perm _ _ _
case intro.mk.intro.intro.mpr.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
hc : ∀ (f : Perm α), f ∈ l → IsCycle f
hd : List.Pairwise Disjoint l
hp : List.prod l = σ
⊢ List.prod l' = List.prod l
case intro.mk.intro.intro.mpr.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
hc : ∀ (f : Perm α), f ∈ l → IsCycle f
hd : List.Pairwise Disjoint l
hp : List.prod l = σ
⊢ l' ~ l
refine' list_cycles_perm_list_cycles _ hc' hc hd' hd
no goals
case intro.mk.intro.intro.mpr.intro.intro
ι : Type ?u.2680422
α : Type u_1
β : Type ?u.2680428
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hn : List.Nodup l
l' : List (Perm α)
hp' : List.prod l' = σ
hc' : ∀ (g : Perm α), g ∈ l' → IsCycle g
hd' : List.Pairwise Disjoint l'
hl :
  Trunc.mk
      { val := l',
        property := (_ : List.prod l' = σ ∧ (∀ (g : Perm α), g ∈ l' → IsCycle g) ∧ List.Pairwise Disjoint l') } =
    truncCycleFactors σ
ht : cycleFactorsFinset σ = List.toFinset l'
hc : ∀ (f : Perm α), f ∈ l → IsCycle f
hd : List.Pairwise Disjoint l
hp : List.prod l = σ
⊢ List.prod l' = List.prod l
rw [hp, hp']