α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ ¬2 ≤ a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ filter (fun n => 2 ≤ n) (partition σ).parts = cycleType σ
rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
  Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ ¬2 ≤ 1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ ¬2 ≤ a
rw [Multiset.eq_of_mem_replicate h]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ ¬2 ≤ 1
decide