no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
⊢ cycleType (g * f⁻¹) + cycleType f = cycleType g - cycleType f + cycleType f
rw [← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType, inv_mul_cancel_right,
  tsub_add_cancel_of_le (cycleType_le_of_mem_cycleFactorsFinset hf)]