α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ map (Finset.card ∘ support) (cycleFactorsFinset σ).val = map (Finset.card ∘ support) s.val
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ cycleType σ = map (Finset.card ∘ support) s.val
rw [cycleType_def]
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ cycleFactorsFinset σ = s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ map (Finset.card ∘ support) (cycleFactorsFinset σ).val = map (Finset.card ∘ support) s.val
congr
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ (∀ (f : Perm α), f ∈ s → IsCycle f) ∧
    ∃ h, Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ cycleFactorsFinset σ = s
rw [cycleFactorsFinset_eq_finset]
no goals
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ (∀ (f : Perm α), f ∈ s → IsCycle f) ∧
    ∃ h, Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
exact ⟨h1, h2, h0⟩