no goals
ι : Type ?u.2748424
α : Type u_1
β : Type ?u.2748430
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
⊢ cycleFactorsFinset f = ∅ ↔ f = 1
simpa [cycleFactorsFinset_eq_finset] using eq_comm