case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ cycleType σ = cycleType (π * σ * π⁻¹)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : IsConj σ τ
⊢ cycleType σ = cycleType τ
obtain ⟨π, rfl⟩ := isConj_iff.1 h
no goals
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ cycleType σ = cycleType (π * σ * π⁻¹)
rw [cycleType_conj]