case pos
ι : Type ?u.2436705
α : Type u_1
β : Type ?u.2436711
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : IsCycle f
hx : ↑f x = x
⊢ cycleOf f x = if ↑f x = x then 1 else f

case neg
ι : Type ?u.2436705
α : Type u_1
β : Type ?u.2436711
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : IsCycle f
hx : ¬↑f x = x
⊢ cycleOf f x = if ↑f x = x then 1 else f
ι : Type ?u.2436705
α : Type u_1
β : Type ?u.2436711
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : IsCycle f
⊢ cycleOf f x = if ↑f x = x then 1 else f
by_cases hx : f x = x
no goals
case pos
ι : Type ?u.2436705
α : Type u_1
β : Type ?u.2436711
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : IsCycle f
hx : ↑f x = x
⊢ cycleOf f x = if ↑f x = x then 1 else f
rwa [if_pos hx, cycleOf_eq_one_iff]
no goals
case neg
ι : Type ?u.2436705
α : Type u_1
β : Type ?u.2436711
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : IsCycle f
hx : ¬↑f x = x
⊢ cycleOf f x = if ↑f x = x then 1 else f
rwa [if_neg hx, hf.cycleOf_eq]