case intro.intro
ι : Type ?u.2683291
α : Type u_1
β : Type ?u.2683297
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hl : List.Nodup l
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ List.toFinset l → IsCycle f) ∧
      ∃ h,
        noncommProd (List.toFinset l) id (_ : Set.Pairwise ↑(List.toFinset l) fun a b => _root_.Commute (id a) (id b)) =
          σ
ι : Type ?u.2683291
α : Type u_1
β : Type ?u.2683297
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
s : Finset (Perm α)
⊢ cycleFactorsFinset σ = s ↔
    (∀ (f : Perm α), f ∈ s → IsCycle f) ∧
      ∃ h, noncommProd s id (_ : Set.Pairwise ↑s fun a b => _root_.Commute (id a) (id b)) = σ
obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
no goals
case intro.intro
ι : Type ?u.2683291
α : Type u_1
β : Type ?u.2683297
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f σ : Perm α
l : List (Perm α)
hl : List.Nodup l
⊢ cycleFactorsFinset σ = List.toFinset l ↔
    (∀ (f : Perm α), f ∈ List.toFinset l → IsCycle f) ∧
      ∃ h,
        noncommProd (List.toFinset l) id (_ : Set.Pairwise ↑(List.toFinset l) fun a b => _root_.Commute (id a) (id b)) =
          σ
simp [cycleFactorsFinset_eq_list_toFinset, hl]