ι : Type ?u.2113579
α : Type u_1
β : Type ?u.2113585
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
⊢ y =
    if SameCycle f x (if SameCycle f⁻¹ x y then ↑f⁻¹ y else y) then ↑f (if SameCycle f⁻¹ x y then ↑f⁻¹ y else y)
    else if SameCycle f⁻¹ x y then ↑f⁻¹ y else y
ι : Type ?u.2113579
α : Type u_1
β : Type ?u.2113585
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
⊢ ↑(cycleOf f x)⁻¹ y = ↑(cycleOf f⁻¹ x) y
rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
no goals
ι : Type ?u.2113579
α : Type u_1
β : Type ?u.2113585
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
⊢ y =
    if SameCycle f x (if SameCycle f⁻¹ x y then ↑f⁻¹ y else y) then ↑f (if SameCycle f⁻¹ x y then ↑f⁻¹ y else y)
    else if SameCycle f⁻¹ x y then ↑f⁻¹ y else y
split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]