case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ Cycle.Nodup (toCycle f hf)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : IsCycle f
⊢ Cycle.Nodup (toCycle f hf)
obtain ⟨x, hx, -⟩ := id hf
no goals
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
⊢ Cycle.Nodup (toCycle f hf)
simpa [toCycle_eq_toList f hf x hx] using nodup_toList _ _