α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ cycleType σ = ↑(List.map (Finset.card ∘ support) l)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
⊢ cycleType σ = ↑(List.map (Finset.card ∘ support) l)
have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ map (Finset.card ∘ support) (List.toFinset l).val = ↑(List.map (Finset.card ∘ support) l)

case h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ ∀ (f : Perm α), f ∈ List.toFinset l → IsCycle f

case h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ Set.Pairwise (↑(List.toFinset l)) Disjoint

case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ Finset.noncommProd (List.toFinset l) id (_ : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (id a) (id b)) = σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ cycleType σ = ↑(List.map (Finset.card ∘ support) l)
rw [cycleType_eq' l.toFinset]
no goals
case h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ ∀ (f : Perm α), f ∈ List.toFinset l → IsCycle f
simpa using h1
no goals
case h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ Set.Pairwise (↑(List.toFinset l)) Disjoint
simpa [hl] using h2
no goals
case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ Finset.noncommProd (List.toFinset l) id (_ : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (id a) (id b)) = σ
simp [hl, h0]