α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : Disjoint σ τ
⊢ Multiset.Disjoint (cycleFactorsFinset σ).val (cycleFactorsFinset τ).val
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : Disjoint σ τ
⊢ Perm.cycleType (σ * τ) = Perm.cycleType σ + Perm.cycleType τ
rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ←
  Multiset.map_add, Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : Disjoint σ τ
⊢ Multiset.Disjoint (cycleFactorsFinset σ).val (cycleFactorsFinset τ).val
exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset