no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ cycleType (τ * σ * τ⁻¹) = cycleType σ
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
| induction_disjoint σ π hd _ hσ hπ =>
  rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]
no goals
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
⊢ cycleType (τ * 1 * τ⁻¹) = cycleType 1
simp
no goals
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ : Perm α
hσ : IsCycle σ
⊢ cycleType (τ * σ * τ⁻¹) = cycleType σ
rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
no goals
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : Disjoint σ π
a✝ : IsCycle σ
hσ : cycleType (τ * σ * τ⁻¹) = cycleType σ
hπ : cycleType (τ * π * τ⁻¹) = cycleType π
⊢ cycleType (τ * (σ * π) * τ⁻¹) = cycleType (σ * π)
rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]