ι : Type ?u.2582968
α : Type u_1
β : Type ?u.2582974
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
hx : IsCycle (cycleOf f x)
⊢ ↑f x ≠ x
ι : Type ?u.2582968
α : Type u_1
β : Type ?u.2582974
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
⊢ IsCycle (cycleOf f x) ↔ ↑f x ≠ x
refine' ⟨fun hx => _, f.isCycle_cycleOf⟩
ι : Type ?u.2582968
α : Type u_1
β : Type ?u.2582974
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
hx : IsCycle (cycleOf f x)
⊢ ¬cycleOf f x = 1
ι : Type ?u.2582968
α : Type u_1
β : Type ?u.2582974
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
hx : IsCycle (cycleOf f x)
⊢ ↑f x ≠ x
rw [Ne.def, ← cycleOf_eq_one_iff f]
no goals
ι : Type ?u.2582968
α : Type u_1
β : Type ?u.2582974
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x y : α
f : Perm α
hx : IsCycle (cycleOf f x)
⊢ ¬cycleOf f x = 1
exact hx.ne_one