α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ cycleType σ = cycleType τ ↔ partition σ = partition τ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ partition σ = partition τ
rw [isConj_iff_cycleType_eq]
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : cycleType σ = cycleType τ
⊢ partition σ = partition τ

case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : partition σ = partition τ
⊢ cycleType σ = cycleType τ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ cycleType σ = cycleType τ ↔ partition σ = partition τ
refine' ⟨fun h => _, fun h => _⟩
no goals
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : cycleType σ = cycleType τ
⊢ partition σ = partition τ
rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
  h]
no goals
case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : partition σ = partition τ
⊢ cycleType σ = cycleType τ
rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]