no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ : Perm α
hσ : IsCycle σ
⊢ (fun τ => cycleType τ⁻¹ = cycleType τ) σ
simp only [hσ.cycleType, hσ.inv.cycleType, support_inv]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ τ : Perm α
hστ : Disjoint σ τ
x✝ : IsCycle σ
hσ : (fun τ => cycleType τ⁻¹ = cycleType τ) σ
hτ : (fun τ => cycleType τ⁻¹ = cycleType τ) τ
⊢ (fun τ => cycleType τ⁻¹ = cycleType τ) (σ * τ)
simp only [mul_inv_rev, hστ.cycleType, hστ.symm.inv_left.inv_right.cycleType, hσ, hτ,
  add_comm]