diff --git a/Mathlib.lean b/Mathlib.lean
index 214ff0b3c8f54..72ad05b0c19fb 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2333,13 +2333,16 @@ import Mathlib.GroupTheory.Order.Min
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.GroupTheory.PGroup
 import Mathlib.GroupTheory.Perm.Basic
+import Mathlib.GroupTheory.Perm.Closure
 import Mathlib.GroupTheory.Perm.ClosureSwap
 import Mathlib.GroupTheory.Perm.Cycle.Basic
 import Mathlib.GroupTheory.Perm.Cycle.Concrete
+import Mathlib.GroupTheory.Perm.Cycle.Factors
 import Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
 import Mathlib.GroupTheory.Perm.Cycle.Type
 import Mathlib.GroupTheory.Perm.DomMulAct
 import Mathlib.GroupTheory.Perm.Fin
+import Mathlib.GroupTheory.Perm.Finite
 import Mathlib.GroupTheory.Perm.List
 import Mathlib.GroupTheory.Perm.Option
 import Mathlib.GroupTheory.Perm.Sign
diff --git a/Mathlib/GroupTheory/Perm/Closure.lean b/Mathlib/GroupTheory/Perm/Closure.lean
new file mode 100644
index 0000000000000..5ea10b1355adf
--- /dev/null
+++ b/Mathlib/GroupTheory/Perm/Closure.lean
@@ -0,0 +1,127 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Yaël Dillies
+-/
+
+import Mathlib.GroupTheory.Perm.Cycle.Basic
+
+#align_import group_theory.perm.cycle.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
+
+/-!
+# Closure results for permutation groups
+
+* This file contains several closure results:
+* `closure_isCycle` : The symmetric group is generated by cycles
+* `closure_cycle_adjacent_swap` : The symmetric group is generated by
+    a cycle and an adjacent transposition
+* `closure_cycle_coprime_swap` : The symmetric group is generated by
+    a cycle and a coprime transposition
+* `closure_prime_cycle_swap` : The symmetric group is generated by
+    a prime cycle and a transposition
+
+-/
+
+open Equiv Function Finset
+
+open BigOperators
+
+variable {ι α β : Type*}
+
+namespace Equiv.Perm
+
+section Generation
+
+variable [Finite β]
+
+open Subgroup
+
+theorem closure_isCycle : closure { σ : Perm β | IsCycle σ } = ⊤ := by
+  classical
+    cases nonempty_fintype β
+    exact
+      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))
+#align equiv.perm.closure_is_cycle Equiv.Perm.closure_isCycle
+
+variable [DecidableEq α] [Fintype α]
+
+theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = ⊤) (x : α) :
+    closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤ := by
+  let H := closure ({σ, swap x (σ x)} : Set (Perm α))
+  have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
+  have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
+  have step1 : ∀ n : ℕ, swap ((σ ^ n) x) ((σ ^ (n + 1) : Perm α) x) ∈ H := by
+    intro n
+    induction' n with n ih
+    · exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
+    · convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
+      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ]
+      rfl
+  have step2 : ∀ n : ℕ, swap x ((σ ^ n) x) ∈ H := by
+    intro n
+    induction' n with n ih
+    · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq, swap_self, Set.mem_singleton_iff]
+      convert H.one_mem
+    · by_cases h5 : x = (σ ^ n) x
+      · rw [pow_succ, mul_apply, ← h5]
+        exact h4
+      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
+      · rw [← h6, swap_self]
+        exact H.one_mem
+      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
+      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
+  have step3 : ∀ y : α, swap x y ∈ H := by
+    intro y
+    have hx : x ∈ (⊤ : Finset α) := Finset.mem_univ x
+    rw [← h2, mem_support] at hx
+    have hy : y ∈ (⊤ : Finset α) := Finset.mem_univ y
+    rw [← h2, mem_support] at hy
+    cases' IsCycle.exists_pow_eq h1 hx hy with n hn
+    rw [← hn]
+    exact step2 n
+  have step4 : ∀ y z : α, swap y z ∈ H := by
+    intro y z
+    by_cases h5 : z = x
+    · rw [h5, swap_comm]
+      exact step3 y
+    by_cases h6 : z = y
+    · rw [h6, swap_self]
+      exact H.one_mem
+    rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
+    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
+  rw [eq_top_iff, ← closure_isSwap, closure_le]
+  rintro τ ⟨y, z, _, h6⟩
+  rw [h6]
+  exact step4 y z
+#align equiv.perm.closure_cycle_adjacent_swap Equiv.Perm.closure_cycle_adjacent_swap
+
+theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.Coprime n (Fintype.card α))
+    (h1 : IsCycle σ) (h2 : σ.support = Finset.univ) (x : α) :
+    closure ({σ, swap x ((σ ^ n) x)} : Set (Perm α)) = ⊤ := by
+  rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
+  cases' exists_pow_eq_self_of_coprime h0 with m hm
+  have h2' : (σ ^ n).support = ⊤ := Eq.trans (support_pow_coprime h0) h2
+  have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
+  replace h1' : IsCycle (σ ^ n) :=
+    h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
+  rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]
+  exact
+    ⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n,
+      Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩
+#align equiv.perm.closure_cycle_coprime_swap Equiv.Perm.closure_cycle_coprime_swap
+
+theorem closure_prime_cycle_swap {σ τ : Perm α} (h0 : (Fintype.card α).Prime) (h1 : IsCycle σ)
+    (h2 : σ.support = Finset.univ) (h3 : IsSwap τ) : closure ({σ, τ} : Set (Perm α)) = ⊤ := by
+  obtain ⟨x, y, h4, h5⟩ := h3
+  obtain ⟨i, hi⟩ :=
+    h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
+      (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
+  rw [h5, ← hi]
+  refine'
+    closure_cycle_coprime_swap (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 _)) h1 h2 x
+  cases' h with m hm
+  rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
+    one_apply] at hi
+#align equiv.perm.closure_prime_cycle_swap Equiv.Perm.closure_prime_cycle_swap
+
+end Generation
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
index cdff4bdb51f07..ac2034deff03f 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -3,20 +3,18 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yaël Dillies
 -/
+
 import Mathlib.Algebra.Module.BigOperators
-import Mathlib.Data.Finset.NoncommProd
 import Mathlib.Data.Fintype.Perm
-import Mathlib.Data.Int.ModEq
+import Mathlib.GroupTheory.Perm.Finite
 import Mathlib.GroupTheory.Perm.List
-import Mathlib.GroupTheory.Perm.Sign
-import Mathlib.Logic.Equiv.Fintype
 
 #align_import group_theory.perm.cycle.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
 /-!
-# Cyclic permutations
+# Cycles of a permutation
 
-This file develops the theory of cycles in permutations.
+This file starts the theory of cycles in permutations.
 
 ## Main definitions
 
@@ -28,23 +26,6 @@ In the following, `f : Equiv.Perm β`.
 * `Equiv.Perm.IsCycleOn`: `f` is a cycle on a set `s` when any two points of `s` are related by
   repeated applications of `f`.
 
-The following two definitions require that `β` is a `Fintype`:
-
-* `Equiv.Perm.cycleOf`: `f.cycleOf x` is the cycle of `f` that `x` belongs to.
-* `Equiv.Perm.cycleFactors`: `f.cycleFactors` is a list of disjoint cyclic permutations that
-  multiply to `f`.
-
-## Main results
-
-* This file contains several closure results:
-  - `closure_isCycle` : The symmetric group is generated by cycles
-  - `closure_cycle_adjacent_swap` : The symmetric group is generated by
-    a cycle and an adjacent transposition
-  - `closure_cycle_coprime_swap` : The symmetric group is generated by
-    a cycle and a coprime transposition
-  - `closure_prime_cycle_swap` : The symmetric group is generated by
-    a prime cycle and a transposition
-
 ## Notes
 
 `Equiv.Perm.IsCycle` and `Equiv.Perm.IsCycleOn` are different in three ways:
@@ -64,7 +45,6 @@ namespace Equiv.Perm
 
 /-! ### `SameCycle` -/
 
-
 section SameCycle
 
 variable {f g : Perm α} {p : α → Prop} {x y z : α}
@@ -282,7 +262,6 @@ end SameCycle
 ### `IsCycle`
 -/
 
-
 section IsCycle
 
 variable {f g : Perm α} {x y : α}
@@ -732,8 +711,59 @@ theorem IsCycle.isCycle_pow_pos_of_lt_prime_order [Finite β] {f : Perm β} (hf
 
 end IsCycle
 
-/-! ### `IsCycleOn` -/
+open Equiv
+
+theorem _root_.Int.addLeft_one_isCycle : (Equiv.addLeft 1 : Perm ℤ).IsCycle :=
+  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩
+#align int.add_left_one_is_cycle Int.addLeft_one_isCycle
+
+theorem _root_.Int.addRight_one_isCycle : (Equiv.addRight 1 : Perm ℤ).IsCycle :=
+  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩
+#align int.add_right_one_is_cycle Int.addRight_one_isCycle
+
+section Conjugation
+
+variable [Fintype α] [DecidableEq α] {σ τ : Perm α}
+
+theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : σ.support.card = τ.support.card) :
+    IsConj σ τ := by
+  refine'
+    isConj_of_support_equiv
+      (hσ.zpowersEquivSupport.symm.trans <|
+        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
+      _
+  intro x hx
+  simp only [Perm.mul_apply, Equiv.trans_apply, Equiv.sumCongr_apply]
+  obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
+  apply
+    Eq.trans _
+      (congr rfl (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply n).symm))))
+  apply (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply (n + 1))))).trans _
+  -- This used to be a `simp only` before leanprover/lean4#2644
+  erw [zpowersEquivZPowers_apply, zpowersEquivZPowers_apply]
+  dsimp
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+  erw [pow_succ, Perm.mul_apply]
+#align equiv.perm.is_cycle.is_conj Equiv.Perm.IsCycle.isConj
+
+theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
+    IsConj σ τ ↔ σ.support.card = τ.support.card :=
+  ⟨by
+    intro h
+    obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
+    refine' Finset.card_congr (fun a _ => π a) (fun _ ha => _) (fun _ _ _ _ ab => π.injective ab)
+        fun b hb => _
+    · simp [mem_support.1 ha]
+    · refine' ⟨π⁻¹ b, ⟨_, π.apply_inv_self b⟩⟩
+      contrapose! hb
+      rw [mem_support, Classical.not_not] at hb
+      rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self],
+    hσ.isConj hτ⟩
+#align equiv.perm.is_cycle.is_conj_iff Equiv.Perm.IsCycle.isConj_iff
+
+end Conjugation
 
+/-! ### `IsCycleOn` -/
 
 section IsCycleOn
 
@@ -940,897 +970,19 @@ protected theorem IsCycleOn.countable (hs : f.IsCycleOn s) : s.Countable := by
   · exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)
 #align equiv.perm.is_cycle_on.countable Equiv.Perm.IsCycleOn.countable
 
-end IsCycleOn
-
-/-!
-### `cycleOf`
--/
-
-
-section CycleOf
-
-variable [DecidableEq α] [Fintype α] {f g : Perm α} {x y : α}
-
-/-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/
-def cycleOf (f : Perm α) (x : α) : Perm α :=
-  ofSubtype (subtypePerm f fun _ => sameCycle_apply_right.symm : Perm { y // SameCycle f x y })
-#align equiv.perm.cycle_of Equiv.Perm.cycleOf
-
-theorem cycleOf_apply (f : Perm α) (x y : α) :
-    cycleOf f x y = if SameCycle f x y then f y else y := by
-  dsimp only [cycleOf]
-  split_ifs with h
-  · apply ofSubtype_apply_of_mem
-    exact h
-  · apply ofSubtype_apply_of_not_mem
-    exact h
-#align equiv.perm.cycle_of_apply Equiv.Perm.cycleOf_apply
-
-theorem cycleOf_inv (f : Perm α) (x : α) : (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
-  Equiv.ext fun y => by
-    rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
-    split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]
-#align equiv.perm.cycle_of_inv Equiv.Perm.cycleOf_inv
-
-@[simp]
-theorem cycleOf_pow_apply_self (f : Perm α) (x : α) : ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x := by
-  intro n
-  induction' n with n hn
-  · rfl
-  · rw [pow_succ, mul_apply, cycleOf_apply, hn, if_pos, pow_succ, mul_apply]
-    exact ⟨n, rfl⟩
-#align equiv.perm.cycle_of_pow_apply_self Equiv.Perm.cycleOf_pow_apply_self
-
-@[simp]
-theorem cycleOf_zpow_apply_self (f : Perm α) (x : α) :
-    ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x := by
-  intro z
-  induction' z with z hz
-  · exact cycleOf_pow_apply_self f x z
-  · rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-#align equiv.perm.cycle_of_zpow_apply_self Equiv.Perm.cycleOf_zpow_apply_self
-
-theorem SameCycle.cycleOf_apply : SameCycle f x y → cycleOf f x y = f y :=
-  ofSubtype_apply_of_mem _
-#align equiv.perm.same_cycle.cycle_of_apply Equiv.Perm.SameCycle.cycleOf_apply
-
-theorem cycleOf_apply_of_not_sameCycle : ¬SameCycle f x y → cycleOf f x y = y :=
-  ofSubtype_apply_of_not_mem _
-#align equiv.perm.cycle_of_apply_of_not_same_cycle Equiv.Perm.cycleOf_apply_of_not_sameCycle
-
-theorem SameCycle.cycleOf_eq (h : SameCycle f x y) : cycleOf f x = cycleOf f y := by
-  ext z
-  rw [Equiv.Perm.cycleOf_apply]
-  split_ifs with hz
-  · exact (h.symm.trans hz).cycleOf_apply.symm
-  · exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm
-#align equiv.perm.same_cycle.cycle_of_eq Equiv.Perm.SameCycle.cycleOf_eq
-
-@[simp]
-theorem cycleOf_apply_apply_zpow_self (f : Perm α) (x : α) (k : ℤ) :
-    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
-  rw [SameCycle.cycleOf_apply]
-  · rw [add_comm, zpow_add, zpow_one, mul_apply]
-  · exact ⟨k, rfl⟩
-#align equiv.perm.cycle_of_apply_apply_zpow_self Equiv.Perm.cycleOf_apply_apply_zpow_self
-
-@[simp]
-theorem cycleOf_apply_apply_pow_self (f : Perm α) (x : α) (k : ℕ) :
-    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
-  convert cycleOf_apply_apply_zpow_self f x k using 1
-#align equiv.perm.cycle_of_apply_apply_pow_self Equiv.Perm.cycleOf_apply_apply_pow_self
-
-@[simp]
-theorem cycleOf_apply_apply_self (f : Perm α) (x : α) : cycleOf f x (f x) = f (f x) := by
-  convert cycleOf_apply_apply_pow_self f x 1 using 1
-#align equiv.perm.cycle_of_apply_apply_self Equiv.Perm.cycleOf_apply_apply_self
-
-@[simp]
-theorem cycleOf_apply_self (f : Perm α) (x : α) : cycleOf f x x = f x :=
-  SameCycle.rfl.cycleOf_apply
-#align equiv.perm.cycle_of_apply_self Equiv.Perm.cycleOf_apply_self
-
-theorem IsCycle.cycleOf_eq (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :=
-  Equiv.ext fun y =>
-    if h : SameCycle f x y then by rw [h.cycleOf_apply]
-    else by
-      rw [cycleOf_apply_of_not_sameCycle h,
-        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]
-#align equiv.perm.is_cycle.cycle_of_eq Equiv.Perm.IsCycle.cycleOf_eq
-
-@[simp]
-theorem cycleOf_eq_one_iff (f : Perm α) : cycleOf f x = 1 ↔ f x = x := by
-  simp_rw [ext_iff, cycleOf_apply, one_apply]
-  refine' ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => _⟩
-  by_cases hy : f y = y
-  · rw [hy, ite_self]
-  · exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))
-#align equiv.perm.cycle_of_eq_one_iff Equiv.Perm.cycleOf_eq_one_iff
-
-@[simp]
-theorem cycleOf_self_apply (f : Perm α) (x : α) : cycleOf f (f x) = cycleOf f x :=
-  (sameCycle_apply_right.2 SameCycle.rfl).symm.cycleOf_eq
-#align equiv.perm.cycle_of_self_apply Equiv.Perm.cycleOf_self_apply
-
-@[simp]
-theorem cycleOf_self_apply_pow (f : Perm α) (n : ℕ) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x :=
-  SameCycle.rfl.pow_left.cycleOf_eq
-#align equiv.perm.cycle_of_self_apply_pow Equiv.Perm.cycleOf_self_apply_pow
-
-@[simp]
-theorem cycleOf_self_apply_zpow (f : Perm α) (n : ℤ) (x : α) :
-    cycleOf f ((f ^ n) x) = cycleOf f x :=
-  SameCycle.rfl.zpow_left.cycleOf_eq
-#align equiv.perm.cycle_of_self_apply_zpow Equiv.Perm.cycleOf_self_apply_zpow
-
-protected theorem IsCycle.cycleOf (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f := by
-  by_cases hx : f x = x
-  · rwa [if_pos hx, cycleOf_eq_one_iff]
-  · rwa [if_neg hx, hf.cycleOf_eq]
-#align equiv.perm.is_cycle.cycle_of Equiv.Perm.IsCycle.cycleOf
-
-theorem cycleOf_one (x : α) : cycleOf 1 x = 1 :=
-  (cycleOf_eq_one_iff 1).mpr rfl
-#align equiv.perm.cycle_of_one Equiv.Perm.cycleOf_one
-
-theorem isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x) :=
-  have : cycleOf f x x ≠ x := by rwa [SameCycle.rfl.cycleOf_apply]
-  (isCycle_iff_sameCycle this).2 @fun y =>
-    ⟨fun h => mt h.apply_eq_self_iff.2 this, fun h =>
-      if hxy : SameCycle f x y then
-        let ⟨i, hi⟩ := hxy
-        ⟨i, by rw [cycleOf_zpow_apply_self, hi]⟩
-      else by
-        rw [cycleOf_apply_of_not_sameCycle hxy] at h
-        exact (h rfl).elim⟩
-#align equiv.perm.is_cycle_cycle_of Equiv.Perm.isCycle_cycleOf
-
-@[simp]
-theorem two_le_card_support_cycleOf_iff : 2 ≤ card (cycleOf f x).support ↔ f x ≠ x := by
-  refine' ⟨fun h => _, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
-  contrapose! h
-  rw [← cycleOf_eq_one_iff] at h
-  simp [h]
-#align equiv.perm.two_le_card_support_cycle_of_iff Equiv.Perm.two_le_card_support_cycleOf_iff
-
-@[simp]
-theorem card_support_cycleOf_pos_iff : 0 < card (cycleOf f x).support ↔ f x ≠ x := by
-  rw [← two_le_card_support_cycleOf_iff, ← Nat.succ_le_iff]
-  exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
-#align equiv.perm.card_support_cycle_of_pos_iff Equiv.Perm.card_support_cycleOf_pos_iff
-
-theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) (n : ℕ) (x : α) :
-    (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x := by
-  rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
-#align equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply Equiv.Perm.pow_mod_orderOf_cycleOf_apply
-
-theorem cycleOf_mul_of_apply_right_eq_self (h : Commute f g) (x : α) (hx : g x = x) :
-    (f * g).cycleOf x = f.cycleOf x := by
-  ext y
-  by_cases hxy : (f * g).SameCycle x y
-  · obtain ⟨z, rfl⟩ := hxy
-    rw [cycleOf_apply_apply_zpow_self]
-    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
-  · rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
-    contrapose! hxy
-    obtain ⟨z, rfl⟩ := hxy
-    refine' ⟨z, _⟩
-    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
-#align equiv.perm.cycle_of_mul_of_apply_right_eq_self Equiv.Perm.cycleOf_mul_of_apply_right_eq_self
-
-theorem Disjoint.cycleOf_mul_distrib (h : f.Disjoint g) (x : α) :
-    (f * g).cycleOf x = f.cycleOf x * g.cycleOf x := by
-  cases' (disjoint_iff_eq_or_eq.mp h) x with hfx hgx
-  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
-  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
-#align equiv.perm.disjoint.cycle_of_mul_distrib Equiv.Perm.Disjoint.cycleOf_mul_distrib
-
-theorem support_cycleOf_eq_nil_iff : (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp
-#align equiv.perm.support_cycle_of_eq_nil_iff Equiv.Perm.support_cycleOf_eq_nil_iff
-
-theorem support_cycleOf_le (f : Perm α) (x : α) : support (f.cycleOf x) ≤ support f := by
-  intro y hy
-  rw [mem_support, cycleOf_apply] at hy
-  split_ifs at hy
-  · exact mem_support.mpr hy
-  · exact absurd rfl hy
-#align equiv.perm.support_cycle_of_le Equiv.Perm.support_cycleOf_le
-
-theorem mem_support_cycleOf_iff : y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f := by
-  by_cases hx : f x = x
-  · rw [(cycleOf_eq_one_iff _).mpr hx]
-    simp [hx]
-  · rw [mem_support, cycleOf_apply]
-    split_ifs with hy
-    · simp only [hx, hy, iff_true_iff, Ne.def, not_false_iff, and_self_iff, mem_support]
-      rcases hy with ⟨k, rfl⟩
-      rw [← not_mem_support]
-      simpa using hx
-    · simpa [hx] using hy
-#align equiv.perm.mem_support_cycle_of_iff Equiv.Perm.mem_support_cycleOf_iff
-
-theorem mem_support_cycleOf_iff' (hx : f x ≠ x) : y ∈ support (f.cycleOf x) ↔ SameCycle f x y := by
-  rw [mem_support_cycleOf_iff, and_iff_left (mem_support.2 hx)]
-#align equiv.perm.mem_support_cycle_of_iff' Equiv.Perm.mem_support_cycleOf_iff'
-
-theorem SameCycle.mem_support_iff (h : SameCycle f x y) : x ∈ support f ↔ y ∈ support f :=
-  ⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
-    support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩
-#align equiv.perm.same_cycle.mem_support_iff Equiv.Perm.SameCycle.mem_support_iff
-
-theorem pow_mod_card_support_cycleOf_self_apply (f : Perm α) (n : ℕ) (x : α) :
-    (f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x := by
-  by_cases hx : f x = x
-  · rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
-  · rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
-      pow_mod_orderOf]
-#align equiv.perm.pow_mod_card_support_cycle_of_self_apply Equiv.Perm.pow_mod_card_support_cycleOf_self_apply
-
-/-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle. -/
-theorem isCycle_cycleOf_iff (f : Perm α) : IsCycle (cycleOf f x) ↔ f x ≠ x := by
-  refine' ⟨fun hx => _, f.isCycle_cycleOf⟩
-  rw [Ne.def, ← cycleOf_eq_one_iff f]
-  exact hx.ne_one
-#align equiv.perm.is_cycle_cycle_of_iff Equiv.Perm.isCycle_cycleOf_iff
-
-theorem isCycleOn_support_cycleOf (f : Perm α) (x : α) : f.IsCycleOn (f.cycleOf x).support :=
-  ⟨f.bijOn <| by
-    refine fun _ ↦ ⟨fun h ↦ mem_support_cycleOf_iff.2 ?_, fun h ↦ mem_support_cycleOf_iff.2 ?_⟩
-    · exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff.1 h).1,
-      (mem_support_cycleOf_iff.1 h).2⟩
-    · exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff.1 h).1,
-      (mem_support_cycleOf_iff.1 h).2⟩
-    , fun a ha b hb =>
-      by
-        rw [mem_coe, mem_support_cycleOf_iff] at ha hb
-        exact ha.1.symm.trans hb.1⟩
-#align equiv.perm.is_cycle_on_support_cycle_of Equiv.Perm.isCycleOn_support_cycleOf
-
-theorem SameCycle.exists_pow_eq_of_mem_support (h : SameCycle f x y) (hx : x ∈ f.support) :
-    ∃ i < (f.cycleOf x).support.card, (f ^ i) x = y := by
-  rw [mem_support] at hx
-  exact Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf x)
-    (by rw [mem_support_cycleOf_iff' hx]) (by rwa [mem_support_cycleOf_iff' hx])
-#align equiv.perm.same_cycle.exists_pow_eq_of_mem_support Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support
-
-theorem SameCycle.exists_pow_eq (f : Perm α) (h : SameCycle f x y) :
-    ∃ i : ℕ, 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y := by
-  by_cases hx : x ∈ f.support
-  · obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
-    cases' k with k
-    · refine' ⟨(f.cycleOf x).support.card, _, self_le_add_right _ _, _⟩
-      · refine' zero_lt_one.trans (one_lt_card_support_of_ne_one _)
-        simpa using hx
-      · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq] at hk'
-        subst hk'
-        rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
-          pow_orderOf_eq_one, one_apply]
-    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
-  · refine' ⟨1, zero_lt_one, by simp, _⟩
-    obtain ⟨k, rfl⟩ := h
-    rw [not_mem_support] at hx
-    rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
-#align equiv.perm.same_cycle.exists_pow_eq Equiv.Perm.SameCycle.exists_pow_eq
-
-end CycleOf
-
-/-!
-### `cycleFactors`
--/
 
-open scoped List in
-/-- Given a list `l : List α` and a permutation `f : perm α` whose nonfixed points are all in `l`,
-  recursively factors `f` into cycles. -/
-def cycleFactorsAux [DecidableEq α] [Fintype α] :
-    ∀ (l : List α) (f : Perm α),
-      (∀ {x}, f x ≠ x → x ∈ l) →
-        { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } := by
-  intro l f h
-  exact match l with
-  | [] => ⟨[], by
-      { simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true_iff,
-          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
-        ext
-        simp [*]}⟩
-  | x::l =>
-    if hx : f x = x then cycleFactorsAux l f (by
-        intro y hy; exact List.mem_of_ne_of_mem (fun h => hy (by rwa [h])) (h hy))
-    else
-      let ⟨m, hm₁, hm₂, hm₃⟩ :=
-        cycleFactorsAux l ((cycleOf f x)⁻¹ * f) (by
-        intro y hy
-        exact List.mem_of_ne_of_mem
-            (fun h : y = x => by
-              rw [h, mul_apply, Ne.def, inv_eq_iff_eq, cycleOf_apply_self] at hy
-              exact hy rfl)
-            (h fun h : f y = y => by
-              rw [mul_apply, h, Ne.def, inv_eq_iff_eq, cycleOf_apply] at hy
-              split_ifs at hy <;> tauto))
-      ⟨cycleOf f x::m, by
-        rw [List.prod_cons, hm₁]
-        simp,
-        fun g hg ↦ ((List.mem_cons).1 hg).elim (fun hg => hg.symm ▸ isCycle_cycleOf _ hx) (hm₂ g),
-        List.pairwise_cons.2
-          ⟨fun g hg y =>
-            or_iff_not_imp_left.2 fun hfy =>
-              have hxy : SameCycle f x y :=
-                Classical.not_not.1 (mt cycleOf_apply_of_not_sameCycle hfy)
-              have hgm : (g::m.erase g) ~ m :=
-                List.cons_perm_iff_perm_erase.2 ⟨hg, List.Perm.refl _⟩
-              have : ∀ h ∈ m.erase g, Disjoint g h :=
-                (List.pairwise_cons.1
-                    ((hgm.pairwise_iff @fun a b (h : Disjoint a b) => h.symm).2 hm₃)).1
-              by_cases id fun hgy : g y ≠ y =>
-                (disjoint_prod_right _ this y).resolve_right <| by
-                  have hsc : SameCycle f⁻¹ x (f y) := by
-                    rwa [sameCycle_inv, sameCycle_apply_right]
-                  rw [disjoint_prod_perm hm₃ hgm.symm, List.prod_cons,
-                      ← eq_inv_mul_iff_mul_eq] at hm₁
-                  rwa [hm₁, mul_apply, mul_apply, cycleOf_inv, hsc.cycleOf_apply, inv_apply_self,
-                    inv_eq_iff_eq, eq_comm],
-            hm₃⟩⟩
-#align equiv.perm.cycle_factors_aux Equiv.Perm.cycleFactorsAux
-
-theorem mem_list_cycles_iff {α : Type*} [Finite α] {l : List (Perm α)}
-    (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) {σ : Perm α} :
-    σ ∈ l ↔ σ.IsCycle ∧ ∀ a, σ a ≠ a → σ a = l.prod a := by
-  suffices σ.IsCycle → (σ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
-    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
-  intro h3
-  classical
-    cases nonempty_fintype α
-    constructor
-    · intro h a ha
-      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
-    · intro h
-      have hσl : σ.support ⊆ l.prod.support := by
-        intro x hx
-        rw [mem_support] at hx
-        rwa [mem_support, ← h _ hx]
-      obtain ⟨a, ha, -⟩ := id h3
-      rw [← mem_support] at ha
-      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
-      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
-      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
-        intro x hx
-        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
-      convert hτ
-      refine' h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key _ ha
-      exact key a (mem_inter_of_mem ha hτa)
-#align equiv.perm.mem_list_cycles_iff Equiv.Perm.mem_list_cycles_iff
-
-open scoped List in
-theorem list_cycles_perm_list_cycles {α : Type*} [Finite α] {l₁ l₂ : List (Perm α)}
-    (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ : Perm α, σ ∈ l₁ → σ.IsCycle)
-    (h₁l₂ : ∀ σ : Perm α, σ ∈ l₂ → σ.IsCycle) (h₂l₁ : l₁.Pairwise Disjoint)
-    (h₂l₂ : l₂.Pairwise Disjoint) : l₁ ~ l₂ := by
-  classical
-    refine'
-      (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
-            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
-        fun σ => _
-    by_cases hσ : σ.IsCycle
-    · obtain _ := not_forall.mp (mt ext hσ.ne_one)
-      rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
-    · exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)
-#align equiv.perm.list_cycles_perm_list_cycles Equiv.Perm.list_cycles_perm_list_cycles
-
-/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`. -/
-def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
-    { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
-  cycleFactorsAux (sort (α := α) (· ≤ ·) univ) f (fun {_ _} ↦ (mem_sort _).2 (mem_univ _))
-#align equiv.perm.cycle_factors Equiv.Perm.cycleFactors
-
-/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
-  without a linear order. -/
-def truncCycleFactors [DecidableEq α] [Fintype α] (f : Perm α) :
-    Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
-  Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (cycleFactorsAux l f (h _)))
-    (show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
-#align equiv.perm.trunc_cycle_factors Equiv.Perm.truncCycleFactors
-
-section CycleFactorsFinset
-
-variable [DecidableEq α] [Fintype α] (f : Perm α)
-
-/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
--/
-def cycleFactorsFinset : Finset (Perm α) :=
-  (truncCycleFactors f).lift
-    (fun l : { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } =>
-      l.val.toFinset)
-    fun ⟨_, hl⟩ ⟨_, hl'⟩ =>
-    List.toFinset_eq_of_perm _ _
-      (list_cycles_perm_list_cycles (hl'.left.symm ▸ hl.left) hl.right.left hl'.right.left
-        hl.right.right hl'.right.right)
-#align equiv.perm.cycle_factors_finset Equiv.Perm.cycleFactorsFinset
-
-open scoped List in
-theorem cycleFactorsFinset_eq_list_toFinset {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
-    σ.cycleFactorsFinset = l.toFinset ↔
-      (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ := by
-  obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
-  have ht : cycleFactorsFinset σ = l'.toFinset := by
-    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk]
-  rw [ht]
-  constructor
-  · intro h
-    have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
-    have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
-    refine' ⟨_, _, _⟩
-    · exact fun _ h => hc' _ (hperm.subset h)
-    · have := List.Perm.pairwise_iff (@Disjoint.symmetric _) hperm
-      rwa [this]
-    · rw [← hp', hperm.symm.prod_eq']
-      refine' hd'.imp _
-      exact Disjoint.commute
-  · rintro ⟨hc, hd, hp⟩
-    refine' List.toFinset_eq_of_perm _ _ _
-    refine' list_cycles_perm_list_cycles _ hc' hc hd' hd
-    rw [hp, hp']
-#align equiv.perm.cycle_factors_finset_eq_list_to_finset Equiv.Perm.cycleFactorsFinset_eq_list_toFinset
-
-theorem cycleFactorsFinset_eq_finset {σ : Perm α} {s : Finset (Perm α)} :
-    σ.cycleFactorsFinset = s ↔
-      (∀ f : Perm α, f ∈ s → f.IsCycle) ∧
-        ∃ h : (s : Set (Perm α)).Pairwise Disjoint,
-          s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ := by
-  obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
-  simp [cycleFactorsFinset_eq_list_toFinset, hl]
-#align equiv.perm.cycle_factors_finset_eq_finset Equiv.Perm.cycleFactorsFinset_eq_finset
-
-theorem cycleFactorsFinset_pairwise_disjoint :
-    (cycleFactorsFinset f : Set (Perm α)).Pairwise Disjoint :=
-  (cycleFactorsFinset_eq_finset.mp rfl).2.choose
-#align equiv.perm.cycle_factors_finset_pairwise_disjoint Equiv.Perm.cycleFactorsFinset_pairwise_disjoint
-
-theorem cycleFactorsFinset_mem_commute : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
-  (cycleFactorsFinset_pairwise_disjoint _).mono' fun _ _ => Disjoint.commute
-#align equiv.perm.cycle_factors_finset_mem_commute Equiv.Perm.cycleFactorsFinset_mem_commute
-
-/-- The product of cycle factors is equal to the original `f : perm α`. -/
-theorem cycleFactorsFinset_noncommProd
-    (comm : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
-      cycleFactorsFinset_mem_commute f) :
-    f.cycleFactorsFinset.noncommProd id comm = f :=
-  (cycleFactorsFinset_eq_finset.mp rfl).2.choose_spec
-#align equiv.perm.cycle_factors_finset_noncomm_prod Equiv.Perm.cycleFactorsFinset_noncommProd
-
-theorem mem_cycleFactorsFinset_iff {f p : Perm α} :
-    p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a := by
-  obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
-  rw [← hl']
-  rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
-  simpa [List.mem_toFinset, Ne.def, ← hl'.right.right] using
-    mem_list_cycles_iff hl'.left hl'.right.left
-#align equiv.perm.mem_cycle_factors_finset_iff Equiv.Perm.mem_cycleFactorsFinset_iff
-
-theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} :
-    cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support := by
-  rw [mem_cycleFactorsFinset_iff]
-  constructor
-  · rintro ⟨hc, _⟩
-    contrapose! hc
-    rw [not_mem_support, ← cycleOf_eq_one_iff] at hc
-    simp [hc]
-  · intro hx
-    refine' ⟨isCycle_cycleOf _ (mem_support.mp hx), _⟩
-    intro y hy
-    rw [mem_support] at hy
-    rw [cycleOf_apply]
-    split_ifs with H
-    · rfl
-    · rw [cycleOf_apply_of_not_sameCycle H] at hy
-      contradiction
-#align equiv.perm.cycle_of_mem_cycle_factors_finset_iff Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-
-theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) :
-    p.support ≤ f.support := by
-  rw [mem_cycleFactorsFinset_iff] at h
-  intro x hx
-  rwa [mem_support, ← h.right x hx, ← mem_support]
-#align equiv.perm.mem_cycle_factors_finset_support_le Equiv.Perm.mem_cycleFactorsFinset_support_le
-
-theorem cycleFactorsFinset_eq_empty_iff {f : Perm α} : cycleFactorsFinset f = ∅ ↔ f = 1 := by
-  simpa [cycleFactorsFinset_eq_finset] using eq_comm
-#align equiv.perm.cycle_factors_finset_eq_empty_iff Equiv.Perm.cycleFactorsFinset_eq_empty_iff
-
-@[simp]
-theorem cycleFactorsFinset_one : cycleFactorsFinset (1 : Perm α) = ∅ := by
-  simp [cycleFactorsFinset_eq_empty_iff]
-#align equiv.perm.cycle_factors_finset_one Equiv.Perm.cycleFactorsFinset_one
-
-@[simp]
-theorem cycleFactorsFinset_eq_singleton_self_iff {f : Perm α} :
-    f.cycleFactorsFinset = {f} ↔ f.IsCycle := by simp [cycleFactorsFinset_eq_finset]
-#align equiv.perm.cycle_factors_finset_eq_singleton_self_iff Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff
-
-theorem IsCycle.cycleFactorsFinset_eq_singleton {f : Perm α} (hf : IsCycle f) :
-    f.cycleFactorsFinset = {f} :=
-  cycleFactorsFinset_eq_singleton_self_iff.mpr hf
-#align equiv.perm.is_cycle.cycle_factors_finset_eq_singleton Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton
-
-theorem cycleFactorsFinset_eq_singleton_iff {f g : Perm α} :
-    f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g := by
-  suffices f = g → (g.IsCycle ↔ f.IsCycle) by
-    rw [cycleFactorsFinset_eq_finset]
-    simpa [eq_comm]
-  rintro rfl
-  exact Iff.rfl
-#align equiv.perm.cycle_factors_finset_eq_singleton_iff Equiv.Perm.cycleFactorsFinset_eq_singleton_iff
-
-/-- Two permutations `f g : perm α` have the same cycle factors iff they are the same. -/
-theorem cycleFactorsFinset_injective : Function.Injective (@cycleFactorsFinset α _ _) := by
-  intro f g h
-  rw [← cycleFactorsFinset_noncommProd f]
-  simpa [h] using cycleFactorsFinset_noncommProd g
-#align equiv.perm.cycle_factors_finset_injective Equiv.Perm.cycleFactorsFinset_injective
-
-theorem Disjoint.disjoint_cycleFactorsFinset {f g : Perm α} (h : Disjoint f g) :
-    _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g) := by
-  rw [disjoint_iff_disjoint_support] at h
-  rw [Finset.disjoint_left]
-  intro x hx hy
-  simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy
-  obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
-  have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
-  tauto
-#align equiv.perm.disjoint.disjoint_cycle_factors_finset Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset
-
-theorem Disjoint.cycleFactorsFinset_mul_eq_union {f g : Perm α} (h : Disjoint f g) :
-    cycleFactorsFinset (f * g) = cycleFactorsFinset f ∪ cycleFactorsFinset g := by
-  rw [cycleFactorsFinset_eq_finset]
-  refine' ⟨_, _, _⟩
-  · simp [or_imp, mem_cycleFactorsFinset_iff, forall_swap]
-  · rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]
-    exact
-      ⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
-        fun x hx y hy _ =>
-        h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩
-  · rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]
-    rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]
-#align equiv.perm.disjoint.cycle_factors_finset_mul_eq_union Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union
-
-theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cycleFactorsFinset g) :
-    Disjoint (g * f⁻¹) f := by
-  rw [mem_cycleFactorsFinset_iff] at h
-  intro x
-  by_cases hx : f x = x
-  · exact Or.inr hx
-  · refine' Or.inl _
-    rw [mul_apply, ← h.right, apply_inv_self]
-    rwa [← support_inv, apply_mem_support, support_inv, mem_support]
-#align equiv.perm.disjoint_mul_inv_of_mem_cycle_factors_finset Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset
-
-/-- If c is a cycle, a ∈ c.support and c is a cycle of f, then `c = f.cycleOf a` -/
-theorem cycle_is_cycleOf {f c : Equiv.Perm α} {a : α} (ha : a ∈ c.support)
-    (hc : c ∈ f.cycleFactorsFinset) : c = f.cycleOf a := by
-  suffices f.cycleOf a = c.cycleOf a by
-    rw [this]
-    apply symm
-    exact
-      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
-        (Equiv.Perm.mem_support.mp ha)
-  let hfc := (Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset hc).symm
-  let hfc2 := Perm.Disjoint.commute hfc
-  rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
-  simp only [hfc2.eq, inv_mul_cancel_right]
-  -- a est dans le support de c, donc pas dans celui de g c⁻¹
-  exact
-    Equiv.Perm.not_mem_support.mp
-      (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)
-#align equiv.perm.cycle_is_cycle_of Equiv.Perm.cycle_is_cycleOf
-
-end CycleFactorsFinset
-
-@[elab_as_elim]
-theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1)
-    (base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ)
-    (induction_disjoint : ∀ σ τ : Perm β,
-      Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ := by
-  cases nonempty_fintype β
-  suffices ∀ l : List (Perm β),
-      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
-    classical
-      let x := σ.truncCycleFactors.out
-      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
-  intro l
-  induction' l with σ l ih
-  · exact fun _ _ => base_one
-  · intro h1 h2
-    rw [List.prod_cons]
-    exact
-      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
-        (h1 _ (List.mem_cons_self _ _)) (base_cycles σ (h1 σ (l.mem_cons_self σ)))
-        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
-#align equiv.perm.cycle_induction_on Equiv.Perm.cycle_induction_on
-
-theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [DecidableEq α] [Fintype α] {f g : Perm α}
-    (h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f} := by
-  revert f
-  refine'
-    cycle_induction_on (P := fun {g : Perm α} ↦
-      ∀ {f}, (f ∈ cycleFactorsFinset g)
-        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ _ _ _
-  · simp
-  · intro σ hσ f hf
-    simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
-    simp [hf]
-  · intro σ τ hd _ hσ hτ f
-    simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
-    -- if only `wlog` could work here...
-    rintro (hf | hf)
-    · rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
-        erase_eq_of_not_mem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
-      · rw [mem_cycleFactorsFinset_iff] at hf
-        intro x
-        cases' hd.symm x with hx hx
-        · exact Or.inl hx
-        · refine' Or.inr _
-          by_cases hfx : f x = x
-          · rw [← hfx]
-            simpa [hx] using hfx.symm
-          · rw [mul_apply]
-            rw [← hf.right _ (mem_support.mpr hfx)] at hx
-            contradiction
-      · exact fun H =>
-        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
-    · rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_not_mem, mul_assoc,
-        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
-      · rw [mem_cycleFactorsFinset_iff] at hf
-        intro x
-        cases' hd x with hx hx
-        · exact Or.inl hx
-        · refine' Or.inr _
-          by_cases hfx : f x = x
-          · rw [← hfx]
-            simpa [hx] using hfx.symm
-          · rw [mul_apply]
-            rw [← hf.right _ (mem_support.mpr hfx)] at hx
-            contradiction
-      · exact fun H =>
-        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))
-#align equiv.perm.cycle_factors_finset_mul_inv_mem_eq_sdiff Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff
-
-section Generation
-
-variable [Finite β]
-
-open Subgroup
-
-theorem closure_isCycle : closure { σ : Perm β | IsCycle σ } = ⊤ := by
-  classical
-    cases nonempty_fintype β
-    exact
-      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))
-#align equiv.perm.closure_is_cycle Equiv.Perm.closure_isCycle
-
-variable [DecidableEq α] [Fintype α]
+end IsCycleOn
 
-theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = ⊤) (x : α) :
-    closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤ := by
-  let H := closure ({σ, swap x (σ x)} : Set (Perm α))
-  have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
-  have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
-  have step1 : ∀ n : ℕ, swap ((σ ^ n) x) ((σ ^ (n + 1) : Perm α) x) ∈ H := by
-    intro n
-    induction' n with n ih
-    · exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
-    · convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
-      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ]
-      rfl
-  have step2 : ∀ n : ℕ, swap x ((σ ^ n) x) ∈ H := by
-    intro n
-    induction' n with n ih
-    · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq, swap_self, Set.mem_singleton_iff]
-      convert H.one_mem
-    · by_cases h5 : x = (σ ^ n) x
-      · rw [pow_succ, mul_apply, ← h5]
-        exact h4
-      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
-      · rw [← h6, swap_self]
-        exact H.one_mem
-      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
-      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
-  have step3 : ∀ y : α, swap x y ∈ H := by
-    intro y
-    have hx : x ∈ (⊤ : Finset α) := Finset.mem_univ x
-    rw [← h2, mem_support] at hx
-    have hy : y ∈ (⊤ : Finset α) := Finset.mem_univ y
-    rw [← h2, mem_support] at hy
-    cases' IsCycle.exists_pow_eq h1 hx hy with n hn
-    rw [← hn]
-    exact step2 n
-  have step4 : ∀ y z : α, swap y z ∈ H := by
-    intro y z
-    by_cases h5 : z = x
-    · rw [h5, swap_comm]
-      exact step3 y
-    by_cases h6 : z = y
-    · rw [h6, swap_self]
-      exact H.one_mem
-    rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
-    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
-  rw [eq_top_iff, ← closure_isSwap, closure_le]
-  rintro τ ⟨y, z, _, h6⟩
-  rw [h6]
-  exact step4 y z
-#align equiv.perm.closure_cycle_adjacent_swap Equiv.Perm.closure_cycle_adjacent_swap
-
-theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.Coprime n (Fintype.card α))
-    (h1 : IsCycle σ) (h2 : σ.support = Finset.univ) (x : α) :
-    closure ({σ, swap x ((σ ^ n) x)} : Set (Perm α)) = ⊤ := by
-  rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
-  cases' exists_pow_eq_self_of_coprime h0 with m hm
-  have h2' : (σ ^ n).support = ⊤ := Eq.trans (support_pow_coprime h0) h2
-  have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
-  replace h1' : IsCycle (σ ^ n) :=
-    h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
-  rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]
-  exact
-    ⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n,
-      Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩
-#align equiv.perm.closure_cycle_coprime_swap Equiv.Perm.closure_cycle_coprime_swap
-
-theorem closure_prime_cycle_swap {σ τ : Perm α} (h0 : (Fintype.card α).Prime) (h1 : IsCycle σ)
-    (h2 : σ.support = Finset.univ) (h3 : IsSwap τ) : closure ({σ, τ} : Set (Perm α)) = ⊤ := by
-  obtain ⟨x, y, h4, h5⟩ := h3
-  obtain ⟨i, hi⟩ :=
-    h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
-      (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
-  rw [h5, ← hi]
-  refine'
-    closure_cycle_coprime_swap (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 _)) h1 h2 x
-  cases' h with m hm
-  rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
-    one_apply] at hi
-#align equiv.perm.closure_prime_cycle_swap Equiv.Perm.closure_prime_cycle_swap
+end Equiv.Perm
 
-end Generation
+namespace List
 
 section
 
-noncomputable section
-
-variable [DecidableEq α] [Fintype α] {σ τ : Perm α}
-
-theorem isConj_of_support_equiv
-    (f : { x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
-    (hf : ∀ (x : α) (hx : x ∈ (σ.support : Set α)),
-      (f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
-    IsConj σ τ := by
-  refine' isConj_iff.2 ⟨Equiv.extendSubtype f, _⟩
-  rw [mul_inv_eq_iff_eq_mul]
-  ext x
-  simp only [Perm.mul_apply]
-  by_cases hx : x ∈ σ.support
-  · rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
-    · exact hf x (Finset.mem_coe.2 hx)
-  · rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
-      Classical.not_not.1 ((not_congr mem_support).mp hx)]
-#align equiv.perm.is_conj_of_support_equiv Equiv.Perm.isConj_of_support_equiv
-
-theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : σ.support.card = τ.support.card) :
-    IsConj σ τ := by
-  refine'
-    isConj_of_support_equiv
-      (hσ.zpowersEquivSupport.symm.trans <|
-        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
-      _
-  intro x hx
-  simp only [Perm.mul_apply, Equiv.trans_apply, Equiv.sumCongr_apply]
-  obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
-  apply
-    Eq.trans _
-      (congr rfl (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply n).symm))))
-  apply (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply (n + 1))))).trans _
-  -- This used to be a `simp only` before leanprover/lean4#2644
-  erw [zpowersEquivZPowers_apply, zpowersEquivZPowers_apply]
-  dsimp
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [pow_succ, Perm.mul_apply]
-#align equiv.perm.is_cycle.is_conj Equiv.Perm.IsCycle.isConj
-
-theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
-    IsConj σ τ ↔ σ.support.card = τ.support.card :=
-  ⟨by
-    intro h
-    obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
-    refine' Finset.card_congr (fun a _ => π a) (fun _ ha => _) (fun _ _ _ _ ab => π.injective ab)
-        fun b hb => _
-    · simp [mem_support.1 ha]
-    · refine' ⟨π⁻¹ b, ⟨_, π.apply_inv_self b⟩⟩
-      contrapose! hb
-      rw [mem_support, Classical.not_not] at hb
-      rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self],
-    hσ.isConj hτ⟩
-#align equiv.perm.is_cycle.is_conj_iff Equiv.Perm.IsCycle.isConj_iff
-
-@[simp]
-theorem support_conj : (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding := by
-  ext
-  simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne.def, Perm.mem_support,
-    Equiv.eq_symm_apply]
-  rfl
-#align equiv.perm.support_conj Equiv.Perm.support_conj
-
-theorem card_support_conj : (σ * τ * σ⁻¹).support.card = τ.support.card := by simp
-#align equiv.perm.card_support_conj Equiv.Perm.card_support_conj
-
-end
-
-theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
-    (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
-  classical
-    cases nonempty_fintype α
-    obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
-    obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
-    have hd1' := coe_inj.2 hd1.support_mul
-    have hd2' := coe_inj.2 hd2.support_mul
-    rw [coe_union] at *
-    have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
-    have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
-    refine' isConj_of_support_equiv _ _
-    · refine'
-          ((Equiv.Set.ofEq hd1').trans (Equiv.Set.union hd1''.le_bot)).trans
-            ((Equiv.sumCongr (subtypeEquiv f fun a => _) (subtypeEquiv g fun a => _)).trans
-              ((Equiv.Set.ofEq hd2').trans (Equiv.Set.union hd2''.le_bot)).symm) <;>
-      · simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
-          apply_eq_iff_eq]
-    · intro x hx
-      simp only [trans_apply, symm_trans_apply, Equiv.Set.ofEq_apply, Equiv.Set.ofEq_symm_apply,
-        Equiv.sumCongr_apply]
-      rw [hd1', Set.mem_union] at hx
-      cases' hx with hxσ hxτ
-      · rw [mem_coe, mem_support] at hxσ
-        rw [Set.union_apply_left hd1''.le_bot _, Set.union_apply_left hd1''.le_bot _]
-        simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
-          Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq]
-        · have h := (hd2 (f x)).resolve_left ?_
-          · rw [mul_apply, mul_apply] at h
-            rw [h, inv_apply_self, (hd1 x).resolve_left hxσ]
-          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
-        · rwa [Subtype.coe_mk, mem_coe, mem_support]
-        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
-            apply_mem_support, mem_support]
-      · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
-        rw [Set.union_apply_right hd1''.le_bot _, Set.union_apply_right hd1''.le_bot _]
-        simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
-          Set.union_symm_apply_right, Subtype.coe_mk, apply_eq_iff_eq]
-        · have h := (hd2 (g (τ x))).resolve_right ?_
-          · rw [mul_apply, mul_apply] at h
-            rw [inv_apply_self, h, (hd1 (τ x)).resolve_right hxτ]
-          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
-        · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
-        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
-            mem_coe, mem_support]
-#align equiv.perm.disjoint.is_conj_mul Equiv.Perm.Disjoint.isConj_mul
-
-section FixedPoints
-
-/-!
-### Fixed points
--/
-
-
-theorem fixed_point_card_lt_of_ne_one [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
-    (filter (fun x => σ x = x) univ).card < Fintype.card α - 1 := by
-  rw [lt_tsub_iff_left, ← lt_tsub_iff_right, ← Finset.card_compl, Finset.compl_filter]
-  exact one_lt_card_support_of_ne_one h
-#align equiv.perm.fixed_point_card_lt_of_ne_one Equiv.Perm.fixed_point_card_lt_of_ne_one
-
-end FixedPoints
-
-end
-
-open Equiv
-
-namespace List
-
 variable [DecidableEq α] {l : List α}
 
 set_option linter.deprecated false in -- nthLe
-theorem _root_.List.Nodup.isCycleOn_formPerm (h : l.Nodup) :
+theorem Nodup.isCycleOn_formPerm (h : l.Nodup) :
     l.formPerm.IsCycleOn { a | a ∈ l } := by
   refine' ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => _⟩
   rw [Set.mem_setOf, ← List.indexOf_lt_length] at ha hb
@@ -1841,27 +993,15 @@ theorem _root_.List.Nodup.isCycleOn_formPerm (h : l.Nodup) :
   rw [add_comm]
 #align list.nodup.is_cycle_on_form_perm List.Nodup.isCycleOn_formPerm
 
-end List
-
-namespace Int
-
-open Equiv
-
-theorem _root_.Int.addLeft_one_isCycle : (Equiv.addLeft 1 : Perm ℤ).IsCycle :=
-  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩
-#align int.add_left_one_is_cycle Int.addLeft_one_isCycle
-
-theorem _root_.Int.addRight_one_isCycle : (Equiv.addRight 1 : Perm ℤ).IsCycle :=
-  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩
-#align int.add_right_one_is_cycle Int.addRight_one_isCycle
+end
 
-end Int
+end List
 
 namespace Finset
 
 variable [DecidableEq α] [Fintype α]
 
-theorem _root_.Finset.exists_cycleOn (s : Finset α) :
+theorem exists_cycleOn (s : Finset α) :
     ∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s := by
   refine ⟨s.toList.formPerm, ?_, fun x hx => by
     simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)⟩
@@ -1875,7 +1015,7 @@ namespace Set
 
 variable {f : Perm α} {s : Set α}
 
-theorem _root_.Set.Countable.exists_cycleOn (hs : s.Countable) :
+theorem Countable.exists_cycleOn (hs : s.Countable) :
     ∃ f : Perm α, f.IsCycleOn s ∧ { x | f x ≠ x } ⊆ s := by
   classical
   obtain hs' | hs' := s.finite_or_infinite
@@ -1894,7 +1034,7 @@ theorem _root_.Set.Countable.exists_cycleOn (hs : s.Countable) :
     simp
 #align set.countable.exists_cycle_on Set.Countable.exists_cycleOn
 
-theorem _root_.Set.prod_self_eq_iUnion_perm (hf : f.IsCycleOn s) :
+theorem prod_self_eq_iUnion_perm (hf : f.IsCycleOn s) :
     s ×ˢ s = ⋃ n : ℤ, (fun a => (a, (f ^ n) a)) '' s := by
   ext ⟨a, b⟩
   simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
@@ -1911,7 +1051,7 @@ namespace Finset
 
 variable {f : Perm α} {s : Finset α}
 
-theorem _root_.Finset.product_self_eq_disjiUnion_perm_aux (hf : f.IsCycleOn s) :
+theorem product_self_eq_disjiUnion_perm_aux (hf : f.IsCycleOn s) :
     (range s.card : Set ℕ).PairwiseDisjoint fun k =>
       s.map ⟨fun i => (i, (f ^ k) i), fun i j => congr_arg Prod.fst⟩ := by
   obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
@@ -1939,7 +1079,7 @@ theorem _root_.Finset.product_self_eq_disjiUnion_perm_aux (hf : f.IsCycleOn s) :
 
 The diagonals are given by the cycle `f`.
 -/
-theorem _root_.Finset.product_self_eq_disjiUnion_perm (hf : f.IsCycleOn s) :
+theorem product_self_eq_disjiUnion_perm (hf : f.IsCycleOn s) :
     s ×ˢ s =
       (range s.card).disjiUnion
         (fun k => s.map ⟨fun i => (i, (f ^ k) i), fun i j => congr_arg Prod.fst⟩)
@@ -1960,13 +1100,13 @@ namespace Finset
 
 variable [Semiring α] [AddCommMonoid β] [Module α β] {s : Finset ι} {σ : Perm ι}
 
-theorem _root_.Finset.sum_smul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
+theorem sum_smul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
     ((∑ i in s, f i) • ∑ i in s, g i) = ∑ k in range s.card, ∑ i in s, f i • g ((σ ^ k) i) := by
   simp_rw [sum_smul_sum, product_self_eq_disjiUnion_perm hσ, sum_disjiUnion, sum_map]
   rfl
 #align finset.sum_smul_sum_eq_sum_perm Finset.sum_smul_sum_eq_sum_perm
 
-theorem _root_.Finset.sum_mul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f g : ι → α) :
+theorem sum_mul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f g : ι → α) :
     ((∑ i in s, f i) * ∑ i in s, g i) = ∑ k in range s.card, ∑ i in s, f i * g ((σ ^ k) i) :=
   sum_smul_sum_eq_sum_perm hσ f g
 #align finset.sum_mul_sum_eq_sum_perm Finset.sum_mul_sum_eq_sum_perm
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean
new file mode 100644
index 0000000000000..0962fa93bfc01
--- /dev/null
+++ b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean
@@ -0,0 +1,693 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Yaël Dillies
+-/
+
+import Mathlib.Algebra.Module.BigOperators
+import Mathlib.Data.Finset.NoncommProd
+import Mathlib.Data.Fintype.Perm
+import Mathlib.Data.Int.ModEq
+import Mathlib.GroupTheory.Perm.List
+import Mathlib.GroupTheory.Perm.Sign
+import Mathlib.Logic.Equiv.Fintype
+
+import Mathlib.GroupTheory.Perm.Cycle.Basic
+
+#align_import group_theory.perm.cycle.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
+
+/-!
+# Cycle factors of a permutation
+
+Let `β` be a `Fintype` and `f : Equiv.Perm β`.
+
+* `Equiv.Perm.cycleOf`: `f.cycleOf x` is the cycle of `f` that `x` belongs to.
+* `Equiv.Perm.cycleFactors`: `f.cycleFactors` is a list of disjoint cyclic permutations
+  that multiply to `f`.
+-/
+
+open Equiv Function Finset
+
+open BigOperators
+
+variable {ι α β : Type*}
+
+namespace Equiv.Perm
+
+/-!
+### `cycleOf`
+-/
+
+section CycleOf
+
+variable [DecidableEq α] [Fintype α] {f g : Perm α} {x y : α}
+
+/-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/
+def cycleOf (f : Perm α) (x : α) : Perm α :=
+  ofSubtype (subtypePerm f fun _ => sameCycle_apply_right.symm : Perm { y // SameCycle f x y })
+#align equiv.perm.cycle_of Equiv.Perm.cycleOf
+
+theorem cycleOf_apply (f : Perm α) (x y : α) :
+    cycleOf f x y = if SameCycle f x y then f y else y := by
+  dsimp only [cycleOf]
+  split_ifs with h
+  · apply ofSubtype_apply_of_mem
+    exact h
+  · apply ofSubtype_apply_of_not_mem
+    exact h
+#align equiv.perm.cycle_of_apply Equiv.Perm.cycleOf_apply
+
+theorem cycleOf_inv (f : Perm α) (x : α) : (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
+  Equiv.ext fun y => by
+    rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
+    split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]
+#align equiv.perm.cycle_of_inv Equiv.Perm.cycleOf_inv
+
+@[simp]
+theorem cycleOf_pow_apply_self (f : Perm α) (x : α) : ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x := by
+  intro n
+  induction' n with n hn
+  · rfl
+  · rw [pow_succ, mul_apply, cycleOf_apply, hn, if_pos, pow_succ, mul_apply]
+    exact ⟨n, rfl⟩
+#align equiv.perm.cycle_of_pow_apply_self Equiv.Perm.cycleOf_pow_apply_self
+
+@[simp]
+theorem cycleOf_zpow_apply_self (f : Perm α) (x : α) :
+    ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x := by
+  intro z
+  induction' z with z hz
+  · exact cycleOf_pow_apply_self f x z
+  · rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
+#align equiv.perm.cycle_of_zpow_apply_self Equiv.Perm.cycleOf_zpow_apply_self
+
+theorem SameCycle.cycleOf_apply : SameCycle f x y → cycleOf f x y = f y :=
+  ofSubtype_apply_of_mem _
+#align equiv.perm.same_cycle.cycle_of_apply Equiv.Perm.SameCycle.cycleOf_apply
+
+theorem cycleOf_apply_of_not_sameCycle : ¬SameCycle f x y → cycleOf f x y = y :=
+  ofSubtype_apply_of_not_mem _
+#align equiv.perm.cycle_of_apply_of_not_same_cycle Equiv.Perm.cycleOf_apply_of_not_sameCycle
+
+theorem SameCycle.cycleOf_eq (h : SameCycle f x y) : cycleOf f x = cycleOf f y := by
+  ext z
+  rw [Equiv.Perm.cycleOf_apply]
+  split_ifs with hz
+  · exact (h.symm.trans hz).cycleOf_apply.symm
+  · exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm
+#align equiv.perm.same_cycle.cycle_of_eq Equiv.Perm.SameCycle.cycleOf_eq
+
+@[simp]
+theorem cycleOf_apply_apply_zpow_self (f : Perm α) (x : α) (k : ℤ) :
+    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
+  rw [SameCycle.cycleOf_apply]
+  · rw [add_comm, zpow_add, zpow_one, mul_apply]
+  · exact ⟨k, rfl⟩
+#align equiv.perm.cycle_of_apply_apply_zpow_self Equiv.Perm.cycleOf_apply_apply_zpow_self
+
+@[simp]
+theorem cycleOf_apply_apply_pow_self (f : Perm α) (x : α) (k : ℕ) :
+    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
+  convert cycleOf_apply_apply_zpow_self f x k using 1
+#align equiv.perm.cycle_of_apply_apply_pow_self Equiv.Perm.cycleOf_apply_apply_pow_self
+
+@[simp]
+theorem cycleOf_apply_apply_self (f : Perm α) (x : α) : cycleOf f x (f x) = f (f x) := by
+  convert cycleOf_apply_apply_pow_self f x 1 using 1
+#align equiv.perm.cycle_of_apply_apply_self Equiv.Perm.cycleOf_apply_apply_self
+
+@[simp]
+theorem cycleOf_apply_self (f : Perm α) (x : α) : cycleOf f x x = f x :=
+  SameCycle.rfl.cycleOf_apply
+#align equiv.perm.cycle_of_apply_self Equiv.Perm.cycleOf_apply_self
+
+theorem IsCycle.cycleOf_eq (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :=
+  Equiv.ext fun y =>
+    if h : SameCycle f x y then by rw [h.cycleOf_apply]
+    else by
+      rw [cycleOf_apply_of_not_sameCycle h,
+        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]
+#align equiv.perm.is_cycle.cycle_of_eq Equiv.Perm.IsCycle.cycleOf_eq
+
+@[simp]
+theorem cycleOf_eq_one_iff (f : Perm α) : cycleOf f x = 1 ↔ f x = x := by
+  simp_rw [ext_iff, cycleOf_apply, one_apply]
+  refine' ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => _⟩
+  by_cases hy : f y = y
+  · rw [hy, ite_self]
+  · exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))
+#align equiv.perm.cycle_of_eq_one_iff Equiv.Perm.cycleOf_eq_one_iff
+
+@[simp]
+theorem cycleOf_self_apply (f : Perm α) (x : α) : cycleOf f (f x) = cycleOf f x :=
+  (sameCycle_apply_right.2 SameCycle.rfl).symm.cycleOf_eq
+#align equiv.perm.cycle_of_self_apply Equiv.Perm.cycleOf_self_apply
+
+@[simp]
+theorem cycleOf_self_apply_pow (f : Perm α) (n : ℕ) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x :=
+  SameCycle.rfl.pow_left.cycleOf_eq
+#align equiv.perm.cycle_of_self_apply_pow Equiv.Perm.cycleOf_self_apply_pow
+
+@[simp]
+theorem cycleOf_self_apply_zpow (f : Perm α) (n : ℤ) (x : α) :
+    cycleOf f ((f ^ n) x) = cycleOf f x :=
+  SameCycle.rfl.zpow_left.cycleOf_eq
+#align equiv.perm.cycle_of_self_apply_zpow Equiv.Perm.cycleOf_self_apply_zpow
+
+protected theorem IsCycle.cycleOf (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f := by
+  by_cases hx : f x = x
+  · rwa [if_pos hx, cycleOf_eq_one_iff]
+  · rwa [if_neg hx, hf.cycleOf_eq]
+#align equiv.perm.is_cycle.cycle_of Equiv.Perm.IsCycle.cycleOf
+
+theorem cycleOf_one (x : α) : cycleOf 1 x = 1 :=
+  (cycleOf_eq_one_iff 1).mpr rfl
+#align equiv.perm.cycle_of_one Equiv.Perm.cycleOf_one
+
+theorem isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x) :=
+  have : cycleOf f x x ≠ x := by rwa [SameCycle.rfl.cycleOf_apply]
+  (isCycle_iff_sameCycle this).2 @fun y =>
+    ⟨fun h => mt h.apply_eq_self_iff.2 this, fun h =>
+      if hxy : SameCycle f x y then
+        let ⟨i, hi⟩ := hxy
+        ⟨i, by rw [cycleOf_zpow_apply_self, hi]⟩
+      else by
+        rw [cycleOf_apply_of_not_sameCycle hxy] at h
+        exact (h rfl).elim⟩
+#align equiv.perm.is_cycle_cycle_of Equiv.Perm.isCycle_cycleOf
+
+@[simp]
+theorem two_le_card_support_cycleOf_iff : 2 ≤ card (cycleOf f x).support ↔ f x ≠ x := by
+  refine' ⟨fun h => _, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
+  contrapose! h
+  rw [← cycleOf_eq_one_iff] at h
+  simp [h]
+#align equiv.perm.two_le_card_support_cycle_of_iff Equiv.Perm.two_le_card_support_cycleOf_iff
+
+@[simp]
+theorem card_support_cycleOf_pos_iff : 0 < card (cycleOf f x).support ↔ f x ≠ x := by
+  rw [← two_le_card_support_cycleOf_iff, ← Nat.succ_le_iff]
+  exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
+#align equiv.perm.card_support_cycle_of_pos_iff Equiv.Perm.card_support_cycleOf_pos_iff
+
+theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) (n : ℕ) (x : α) :
+    (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x := by
+  rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
+#align equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply Equiv.Perm.pow_mod_orderOf_cycleOf_apply
+
+theorem cycleOf_mul_of_apply_right_eq_self (h : Commute f g) (x : α) (hx : g x = x) :
+    (f * g).cycleOf x = f.cycleOf x := by
+  ext y
+  by_cases hxy : (f * g).SameCycle x y
+  · obtain ⟨z, rfl⟩ := hxy
+    rw [cycleOf_apply_apply_zpow_self]
+    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
+  · rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
+    contrapose! hxy
+    obtain ⟨z, rfl⟩ := hxy
+    refine' ⟨z, _⟩
+    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
+#align equiv.perm.cycle_of_mul_of_apply_right_eq_self Equiv.Perm.cycleOf_mul_of_apply_right_eq_self
+
+theorem Disjoint.cycleOf_mul_distrib (h : f.Disjoint g) (x : α) :
+    (f * g).cycleOf x = f.cycleOf x * g.cycleOf x := by
+  cases' (disjoint_iff_eq_or_eq.mp h) x with hfx hgx
+  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
+  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
+#align equiv.perm.disjoint.cycle_of_mul_distrib Equiv.Perm.Disjoint.cycleOf_mul_distrib
+
+theorem support_cycleOf_eq_nil_iff : (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp
+#align equiv.perm.support_cycle_of_eq_nil_iff Equiv.Perm.support_cycleOf_eq_nil_iff
+
+theorem support_cycleOf_le (f : Perm α) (x : α) : support (f.cycleOf x) ≤ support f := by
+  intro y hy
+  rw [mem_support, cycleOf_apply] at hy
+  split_ifs at hy
+  · exact mem_support.mpr hy
+  · exact absurd rfl hy
+#align equiv.perm.support_cycle_of_le Equiv.Perm.support_cycleOf_le
+
+theorem mem_support_cycleOf_iff : y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f := by
+  by_cases hx : f x = x
+  · rw [(cycleOf_eq_one_iff _).mpr hx]
+    simp [hx]
+  · rw [mem_support, cycleOf_apply]
+    split_ifs with hy
+    · simp only [hx, hy, iff_true_iff, Ne.def, not_false_iff, and_self_iff, mem_support]
+      rcases hy with ⟨k, rfl⟩
+      rw [← not_mem_support]
+      simpa using hx
+    · simpa [hx] using hy
+#align equiv.perm.mem_support_cycle_of_iff Equiv.Perm.mem_support_cycleOf_iff
+
+theorem mem_support_cycleOf_iff' (hx : f x ≠ x) : y ∈ support (f.cycleOf x) ↔ SameCycle f x y := by
+  rw [mem_support_cycleOf_iff, and_iff_left (mem_support.2 hx)]
+#align equiv.perm.mem_support_cycle_of_iff' Equiv.Perm.mem_support_cycleOf_iff'
+
+theorem SameCycle.mem_support_iff (h : SameCycle f x y) : x ∈ support f ↔ y ∈ support f :=
+  ⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
+    support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩
+#align equiv.perm.same_cycle.mem_support_iff Equiv.Perm.SameCycle.mem_support_iff
+
+theorem pow_mod_card_support_cycleOf_self_apply (f : Perm α) (n : ℕ) (x : α) :
+    (f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x := by
+  by_cases hx : f x = x
+  · rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
+  · rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
+      pow_mod_orderOf]
+#align equiv.perm.pow_mod_card_support_cycle_of_self_apply Equiv.Perm.pow_mod_card_support_cycleOf_self_apply
+
+/-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle. -/
+theorem isCycle_cycleOf_iff (f : Perm α) : IsCycle (cycleOf f x) ↔ f x ≠ x := by
+  refine' ⟨fun hx => _, f.isCycle_cycleOf⟩
+  rw [Ne.def, ← cycleOf_eq_one_iff f]
+  exact hx.ne_one
+#align equiv.perm.is_cycle_cycle_of_iff Equiv.Perm.isCycle_cycleOf_iff
+
+theorem isCycleOn_support_cycleOf (f : Perm α) (x : α) : f.IsCycleOn (f.cycleOf x).support :=
+  ⟨f.bijOn <| by
+    refine fun _ ↦ ⟨fun h ↦ mem_support_cycleOf_iff.2 ?_, fun h ↦ mem_support_cycleOf_iff.2 ?_⟩
+    · exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff.1 h).1,
+      (mem_support_cycleOf_iff.1 h).2⟩
+    · exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff.1 h).1,
+      (mem_support_cycleOf_iff.1 h).2⟩
+    , fun a ha b hb =>
+      by
+        rw [mem_coe, mem_support_cycleOf_iff] at ha hb
+        exact ha.1.symm.trans hb.1⟩
+#align equiv.perm.is_cycle_on_support_cycle_of Equiv.Perm.isCycleOn_support_cycleOf
+
+theorem SameCycle.exists_pow_eq_of_mem_support (h : SameCycle f x y) (hx : x ∈ f.support) :
+    ∃ i < (f.cycleOf x).support.card, (f ^ i) x = y := by
+  rw [mem_support] at hx
+  exact Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf x)
+    (by rw [mem_support_cycleOf_iff' hx]) (by rwa [mem_support_cycleOf_iff' hx])
+#align equiv.perm.same_cycle.exists_pow_eq_of_mem_support Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support
+
+theorem SameCycle.exists_pow_eq (f : Perm α) (h : SameCycle f x y) :
+    ∃ i : ℕ, 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y := by
+  by_cases hx : x ∈ f.support
+  · obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
+    cases' k with k
+    · refine' ⟨(f.cycleOf x).support.card, _, self_le_add_right _ _, _⟩
+      · refine' zero_lt_one.trans (one_lt_card_support_of_ne_one _)
+        simpa using hx
+      · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq] at hk'
+        subst hk'
+        rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
+          pow_orderOf_eq_one, one_apply]
+    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
+  · refine' ⟨1, zero_lt_one, by simp, _⟩
+    obtain ⟨k, rfl⟩ := h
+    rw [not_mem_support] at hx
+    rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
+#align equiv.perm.same_cycle.exists_pow_eq Equiv.Perm.SameCycle.exists_pow_eq
+
+end CycleOf
+
+
+/-!
+### `cycleFactors`
+-/
+
+section cycleFactors
+
+open scoped List in
+/-- Given a list `l : List α` and a permutation `f : perm α` whose nonfixed points are all in `l`,
+  recursively factors `f` into cycles. -/
+def cycleFactorsAux [DecidableEq α] [Fintype α] :
+    ∀ (l : List α) (f : Perm α),
+      (∀ {x}, f x ≠ x → x ∈ l) →
+        { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } := by
+  intro l f h
+  exact match l with
+  | [] => ⟨[], by
+      { simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true_iff,
+          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
+        ext
+        simp [*]}⟩
+  | x::l =>
+    if hx : f x = x then cycleFactorsAux l f (by
+        intro y hy; exact List.mem_of_ne_of_mem (fun h => hy (by rwa [h])) (h hy))
+    else
+      let ⟨m, hm₁, hm₂, hm₃⟩ :=
+        cycleFactorsAux l ((cycleOf f x)⁻¹ * f) (by
+        intro y hy
+        exact List.mem_of_ne_of_mem
+            (fun h : y = x => by
+              rw [h, mul_apply, Ne.def, inv_eq_iff_eq, cycleOf_apply_self] at hy
+              exact hy rfl)
+            (h fun h : f y = y => by
+              rw [mul_apply, h, Ne.def, inv_eq_iff_eq, cycleOf_apply] at hy
+              split_ifs at hy <;> tauto))
+      ⟨cycleOf f x::m, by
+        rw [List.prod_cons, hm₁]
+        simp,
+        fun g hg ↦ ((List.mem_cons).1 hg).elim (fun hg => hg.symm ▸ isCycle_cycleOf _ hx) (hm₂ g),
+        List.pairwise_cons.2
+          ⟨fun g hg y =>
+            or_iff_not_imp_left.2 fun hfy =>
+              have hxy : SameCycle f x y :=
+                Classical.not_not.1 (mt cycleOf_apply_of_not_sameCycle hfy)
+              have hgm : (g::m.erase g) ~ m :=
+                List.cons_perm_iff_perm_erase.2 ⟨hg, List.Perm.refl _⟩
+              have : ∀ h ∈ m.erase g, Disjoint g h :=
+                (List.pairwise_cons.1
+                    ((hgm.pairwise_iff @fun a b (h : Disjoint a b) => h.symm).2 hm₃)).1
+              by_cases id fun hgy : g y ≠ y =>
+                (disjoint_prod_right _ this y).resolve_right <| by
+                  have hsc : SameCycle f⁻¹ x (f y) := by
+                    rwa [sameCycle_inv, sameCycle_apply_right]
+                  rw [disjoint_prod_perm hm₃ hgm.symm, List.prod_cons,
+                      ← eq_inv_mul_iff_mul_eq] at hm₁
+                  rwa [hm₁, mul_apply, mul_apply, cycleOf_inv, hsc.cycleOf_apply, inv_apply_self,
+                    inv_eq_iff_eq, eq_comm],
+            hm₃⟩⟩
+#align equiv.perm.cycle_factors_aux Equiv.Perm.cycleFactorsAux
+
+theorem mem_list_cycles_iff {α : Type*} [Finite α] {l : List (Perm α)}
+    (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) {σ : Perm α} :
+    σ ∈ l ↔ σ.IsCycle ∧ ∀ a, σ a ≠ a → σ a = l.prod a := by
+  suffices σ.IsCycle → (σ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
+    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
+  intro h3
+  classical
+    cases nonempty_fintype α
+    constructor
+    · intro h a ha
+      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
+    · intro h
+      have hσl : σ.support ⊆ l.prod.support := by
+        intro x hx
+        rw [mem_support] at hx
+        rwa [mem_support, ← h _ hx]
+      obtain ⟨a, ha, -⟩ := id h3
+      rw [← mem_support] at ha
+      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
+      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
+      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
+        intro x hx
+        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
+      convert hτ
+      refine' h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key _ ha
+      exact key a (mem_inter_of_mem ha hτa)
+#align equiv.perm.mem_list_cycles_iff Equiv.Perm.mem_list_cycles_iff
+
+open scoped List in
+theorem list_cycles_perm_list_cycles {α : Type*} [Finite α] {l₁ l₂ : List (Perm α)}
+    (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ : Perm α, σ ∈ l₁ → σ.IsCycle)
+    (h₁l₂ : ∀ σ : Perm α, σ ∈ l₂ → σ.IsCycle) (h₂l₁ : l₁.Pairwise Disjoint)
+    (h₂l₂ : l₂.Pairwise Disjoint) : l₁ ~ l₂ := by
+  classical
+    refine'
+      (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
+            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
+        fun σ => _
+    by_cases hσ : σ.IsCycle
+    · obtain _ := not_forall.mp (mt ext hσ.ne_one)
+      rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
+    · exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)
+#align equiv.perm.list_cycles_perm_list_cycles Equiv.Perm.list_cycles_perm_list_cycles
+
+/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`. -/
+def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
+    { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
+  cycleFactorsAux (sort (α := α) (· ≤ ·) univ) f (fun {_ _} ↦ (mem_sort _).2 (mem_univ _))
+#align equiv.perm.cycle_factors Equiv.Perm.cycleFactors
+
+/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
+  without a linear order. -/
+def truncCycleFactors [DecidableEq α] [Fintype α] (f : Perm α) :
+    Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
+  Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (cycleFactorsAux l f (h _)))
+    (show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
+#align equiv.perm.trunc_cycle_factors Equiv.Perm.truncCycleFactors
+
+section CycleFactorsFinset
+
+variable [DecidableEq α] [Fintype α] (f : Perm α)
+
+/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
+-/
+def cycleFactorsFinset : Finset (Perm α) :=
+  (truncCycleFactors f).lift
+    (fun l : { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } =>
+      l.val.toFinset)
+    fun ⟨_, hl⟩ ⟨_, hl'⟩ =>
+    List.toFinset_eq_of_perm _ _
+      (list_cycles_perm_list_cycles (hl'.left.symm ▸ hl.left) hl.right.left hl'.right.left
+        hl.right.right hl'.right.right)
+#align equiv.perm.cycle_factors_finset Equiv.Perm.cycleFactorsFinset
+
+open scoped List in
+theorem cycleFactorsFinset_eq_list_toFinset {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
+    σ.cycleFactorsFinset = l.toFinset ↔
+      (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ := by
+  obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
+  have ht : cycleFactorsFinset σ = l'.toFinset := by
+    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk]
+  rw [ht]
+  constructor
+  · intro h
+    have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
+    have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
+    refine' ⟨_, _, _⟩
+    · exact fun _ h => hc' _ (hperm.subset h)
+    · have := List.Perm.pairwise_iff (@Disjoint.symmetric _) hperm
+      rwa [this]
+    · rw [← hp', hperm.symm.prod_eq']
+      refine' hd'.imp _
+      exact Disjoint.commute
+  · rintro ⟨hc, hd, hp⟩
+    refine' List.toFinset_eq_of_perm _ _ _
+    refine' list_cycles_perm_list_cycles _ hc' hc hd' hd
+    rw [hp, hp']
+#align equiv.perm.cycle_factors_finset_eq_list_to_finset Equiv.Perm.cycleFactorsFinset_eq_list_toFinset
+
+theorem cycleFactorsFinset_eq_finset {σ : Perm α} {s : Finset (Perm α)} :
+    σ.cycleFactorsFinset = s ↔
+      (∀ f : Perm α, f ∈ s → f.IsCycle) ∧
+        ∃ h : (s : Set (Perm α)).Pairwise Disjoint,
+          s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ := by
+  obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
+  simp [cycleFactorsFinset_eq_list_toFinset, hl]
+#align equiv.perm.cycle_factors_finset_eq_finset Equiv.Perm.cycleFactorsFinset_eq_finset
+
+theorem cycleFactorsFinset_pairwise_disjoint :
+    (cycleFactorsFinset f : Set (Perm α)).Pairwise Disjoint :=
+  (cycleFactorsFinset_eq_finset.mp rfl).2.choose
+#align equiv.perm.cycle_factors_finset_pairwise_disjoint Equiv.Perm.cycleFactorsFinset_pairwise_disjoint
+
+theorem cycleFactorsFinset_mem_commute : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
+  (cycleFactorsFinset_pairwise_disjoint _).mono' fun _ _ => Disjoint.commute
+#align equiv.perm.cycle_factors_finset_mem_commute Equiv.Perm.cycleFactorsFinset_mem_commute
+
+/-- The product of cycle factors is equal to the original `f : perm α`. -/
+theorem cycleFactorsFinset_noncommProd
+    (comm : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
+      cycleFactorsFinset_mem_commute f) :
+    f.cycleFactorsFinset.noncommProd id comm = f :=
+  (cycleFactorsFinset_eq_finset.mp rfl).2.choose_spec
+#align equiv.perm.cycle_factors_finset_noncomm_prod Equiv.Perm.cycleFactorsFinset_noncommProd
+
+theorem mem_cycleFactorsFinset_iff {f p : Perm α} :
+    p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a := by
+  obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
+  rw [← hl']
+  rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
+  simpa [List.mem_toFinset, Ne.def, ← hl'.right.right] using
+    mem_list_cycles_iff hl'.left hl'.right.left
+#align equiv.perm.mem_cycle_factors_finset_iff Equiv.Perm.mem_cycleFactorsFinset_iff
+
+theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} :
+    cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support := by
+  rw [mem_cycleFactorsFinset_iff]
+  constructor
+  · rintro ⟨hc, _⟩
+    contrapose! hc
+    rw [not_mem_support, ← cycleOf_eq_one_iff] at hc
+    simp [hc]
+  · intro hx
+    refine' ⟨isCycle_cycleOf _ (mem_support.mp hx), _⟩
+    intro y hy
+    rw [mem_support] at hy
+    rw [cycleOf_apply]
+    split_ifs with H
+    · rfl
+    · rw [cycleOf_apply_of_not_sameCycle H] at hy
+      contradiction
+#align equiv.perm.cycle_of_mem_cycle_factors_finset_iff Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
+
+theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) :
+    p.support ≤ f.support := by
+  rw [mem_cycleFactorsFinset_iff] at h
+  intro x hx
+  rwa [mem_support, ← h.right x hx, ← mem_support]
+#align equiv.perm.mem_cycle_factors_finset_support_le Equiv.Perm.mem_cycleFactorsFinset_support_le
+
+theorem cycleFactorsFinset_eq_empty_iff {f : Perm α} : cycleFactorsFinset f = ∅ ↔ f = 1 := by
+  simpa [cycleFactorsFinset_eq_finset] using eq_comm
+#align equiv.perm.cycle_factors_finset_eq_empty_iff Equiv.Perm.cycleFactorsFinset_eq_empty_iff
+
+@[simp]
+theorem cycleFactorsFinset_one : cycleFactorsFinset (1 : Perm α) = ∅ := by
+  simp [cycleFactorsFinset_eq_empty_iff]
+#align equiv.perm.cycle_factors_finset_one Equiv.Perm.cycleFactorsFinset_one
+
+@[simp]
+theorem cycleFactorsFinset_eq_singleton_self_iff {f : Perm α} :
+    f.cycleFactorsFinset = {f} ↔ f.IsCycle := by simp [cycleFactorsFinset_eq_finset]
+#align equiv.perm.cycle_factors_finset_eq_singleton_self_iff Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff
+
+theorem IsCycle.cycleFactorsFinset_eq_singleton {f : Perm α} (hf : IsCycle f) :
+    f.cycleFactorsFinset = {f} :=
+  cycleFactorsFinset_eq_singleton_self_iff.mpr hf
+#align equiv.perm.is_cycle.cycle_factors_finset_eq_singleton Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton
+
+theorem cycleFactorsFinset_eq_singleton_iff {f g : Perm α} :
+    f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g := by
+  suffices f = g → (g.IsCycle ↔ f.IsCycle) by
+    rw [cycleFactorsFinset_eq_finset]
+    simpa [eq_comm]
+  rintro rfl
+  exact Iff.rfl
+#align equiv.perm.cycle_factors_finset_eq_singleton_iff Equiv.Perm.cycleFactorsFinset_eq_singleton_iff
+
+/-- Two permutations `f g : perm α` have the same cycle factors iff they are the same. -/
+theorem cycleFactorsFinset_injective : Function.Injective (@cycleFactorsFinset α _ _) := by
+  intro f g h
+  rw [← cycleFactorsFinset_noncommProd f]
+  simpa [h] using cycleFactorsFinset_noncommProd g
+#align equiv.perm.cycle_factors_finset_injective Equiv.Perm.cycleFactorsFinset_injective
+
+theorem Disjoint.disjoint_cycleFactorsFinset {f g : Perm α} (h : Disjoint f g) :
+    _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g) := by
+  rw [disjoint_iff_disjoint_support] at h
+  rw [Finset.disjoint_left]
+  intro x hx hy
+  simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy
+  obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
+  have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
+  tauto
+#align equiv.perm.disjoint.disjoint_cycle_factors_finset Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset
+
+theorem Disjoint.cycleFactorsFinset_mul_eq_union {f g : Perm α} (h : Disjoint f g) :
+    cycleFactorsFinset (f * g) = cycleFactorsFinset f ∪ cycleFactorsFinset g := by
+  rw [cycleFactorsFinset_eq_finset]
+  refine' ⟨_, _, _⟩
+  · simp [or_imp, mem_cycleFactorsFinset_iff, forall_swap]
+  · rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]
+    exact
+      ⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
+        fun x hx y hy _ =>
+        h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩
+  · rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]
+    rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]
+#align equiv.perm.disjoint.cycle_factors_finset_mul_eq_union Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union
+
+theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cycleFactorsFinset g) :
+    Disjoint (g * f⁻¹) f := by
+  rw [mem_cycleFactorsFinset_iff] at h
+  intro x
+  by_cases hx : f x = x
+  · exact Or.inr hx
+  · refine' Or.inl _
+    rw [mul_apply, ← h.right, apply_inv_self]
+    rwa [← support_inv, apply_mem_support, support_inv, mem_support]
+#align equiv.perm.disjoint_mul_inv_of_mem_cycle_factors_finset Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset
+
+/-- If c is a cycle, a ∈ c.support and c is a cycle of f, then `c = f.cycleOf a` -/
+theorem cycle_is_cycleOf {f c : Equiv.Perm α} {a : α} (ha : a ∈ c.support)
+    (hc : c ∈ f.cycleFactorsFinset) : c = f.cycleOf a := by
+  suffices f.cycleOf a = c.cycleOf a by
+    rw [this]
+    apply symm
+    exact
+      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
+        (Equiv.Perm.mem_support.mp ha)
+  let hfc := (Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset hc).symm
+  let hfc2 := Perm.Disjoint.commute hfc
+  rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
+  simp only [hfc2.eq, inv_mul_cancel_right]
+  -- a est dans le support de c, donc pas dans celui de g c⁻¹
+  exact
+    Equiv.Perm.not_mem_support.mp
+      (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)
+#align equiv.perm.cycle_is_cycle_of Equiv.Perm.cycle_is_cycleOf
+
+end CycleFactorsFinset
+
+@[elab_as_elim]
+theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1)
+    (base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ)
+    (induction_disjoint : ∀ σ τ : Perm β,
+      Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ := by
+  cases nonempty_fintype β
+  suffices ∀ l : List (Perm β),
+      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
+    classical
+      let x := σ.truncCycleFactors.out
+      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
+  intro l
+  induction' l with σ l ih
+  · exact fun _ _ => base_one
+  · intro h1 h2
+    rw [List.prod_cons]
+    exact
+      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
+        (h1 _ (List.mem_cons_self _ _)) (base_cycles σ (h1 σ (l.mem_cons_self σ)))
+        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
+#align equiv.perm.cycle_induction_on Equiv.Perm.cycle_induction_on
+
+theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [DecidableEq α] [Fintype α] {f g : Perm α}
+    (h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f} := by
+  revert f
+  refine'
+    cycle_induction_on (P := fun {g : Perm α} ↦
+      ∀ {f}, (f ∈ cycleFactorsFinset g)
+        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ _ _ _
+  · simp
+  · intro σ hσ f hf
+    simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
+    simp [hf]
+  · intro σ τ hd _ hσ hτ f
+    simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
+    -- if only `wlog` could work here...
+    rintro (hf | hf)
+    · rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
+        erase_eq_of_not_mem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
+      · rw [mem_cycleFactorsFinset_iff] at hf
+        intro x
+        cases' hd.symm x with hx hx
+        · exact Or.inl hx
+        · refine' Or.inr _
+          by_cases hfx : f x = x
+          · rw [← hfx]
+            simpa [hx] using hfx.symm
+          · rw [mul_apply]
+            rw [← hf.right _ (mem_support.mpr hfx)] at hx
+            contradiction
+      · exact fun H =>
+        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
+    · rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_not_mem, mul_assoc,
+        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
+      · rw [mem_cycleFactorsFinset_iff] at hf
+        intro x
+        cases' hd x with hx hx
+        · exact Or.inl hx
+        · refine' Or.inr _
+          by_cases hfx : f x = x
+          · rw [← hfx]
+            simpa [hx] using hfx.symm
+          · rw [mul_apply]
+            rw [← hf.right _ (mem_support.mpr hfx)] at hx
+            contradiction
+      · exact fun H =>
+        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))
+#align equiv.perm.cycle_factors_finset_mul_inv_mem_eq_sdiff Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff
+
+end cycleFactors
+
+end Perm
+
+end Equiv
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Type.lean b/Mathlib/GroupTheory/Perm/Cycle/Type.lean
index 733d7200d66bc..bd674a6d8b5ce 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Type.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Type.lean
@@ -6,7 +6,8 @@ Authors: Thomas Browning
 import Mathlib.Algebra.GCDMonoid.Multiset
 import Mathlib.Combinatorics.Partition
 import Mathlib.Data.List.Rotate
-import Mathlib.GroupTheory.Perm.Cycle.Basic
+import Mathlib.GroupTheory.Perm.Cycle.Factors
+import Mathlib.GroupTheory.Perm.Closure
 import Mathlib.RingTheory.Int.Basic
 import Mathlib.Tactic.NormNum.GCD
 
@@ -194,14 +195,14 @@ theorem orderOf_cycleOf_dvd_orderOf (f : Perm α) (x : α) : orderOf (cycleOf f
 theorem two_dvd_card_support {σ : Perm α} (hσ : σ ^ 2 = 1) : 2 ∣ σ.support.card :=
   (congr_arg (Dvd.dvd 2) σ.sum_cycleType).mp
     (Multiset.dvd_sum fun n hn => by
-      rw [le_antisymm
+      rw [_root_.le_antisymm
           (Nat.le_of_dvd zero_lt_two <|
             (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
           (two_le_of_mem_cycleType hn)])
 #align equiv.perm.two_dvd_card_support Equiv.Perm.two_dvd_card_support
 
 theorem cycleType_prime_order {σ : Perm α} (hσ : (orderOf σ).Prime) :
-    ∃ n : ℕ, σ.cycleType = replicate (n + 1) (orderOf σ) := by
+    ∃ n : ℕ, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ) := by
   refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
   · rw [tsub_add_cancel_of_le]
     rw [Nat.succ_le_iff, card_cycleType_pos, Ne.def, ← orderOf_eq_one_iff]
@@ -532,7 +533,7 @@ variable [DecidableEq α]
 
 /-- The partition corresponding to a permutation -/
 def partition (σ : Perm α) : (Fintype.card α).Partition where
-  parts := σ.cycleType + replicate (Fintype.card α - σ.support.card) 1
+  parts := σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1
   parts_pos {n hn} := by
     cases' mem_add.mp hn with hn hn
     · exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)
@@ -543,7 +544,7 @@ def partition (σ : Perm α) : (Fintype.card α).Partition where
 #align equiv.perm.partition Equiv.Perm.partition
 
 theorem parts_partition {σ : Perm α} :
-    σ.partition.parts = σ.cycleType + replicate (Fintype.card α - σ.support.card) 1 :=
+    σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1 :=
   rfl
 #align equiv.perm.parts_partition Equiv.Perm.parts_partition
 
diff --git a/Mathlib/GroupTheory/Perm/Finite.lean b/Mathlib/GroupTheory/Perm/Finite.lean
new file mode 100644
index 0000000000000..2b6105ab46d5f
--- /dev/null
+++ b/Mathlib/GroupTheory/Perm/Finite.lean
@@ -0,0 +1,253 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Mathlib.Data.Finset.Fin
+import Mathlib.Data.Int.Order.Units
+import Mathlib.GroupTheory.OrderOfElement
+import Mathlib.GroupTheory.Perm.Support
+import Mathlib.Logic.Equiv.Fintype
+
+#align_import group_theory.perm.sign from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
+
+/-!
+# Permutations on `Fintype`s
+
+This file contains miscellaneous lemmas about `Equiv.Perm` and `Equiv.swap`, building on top
+of those in `Data/Equiv/Basic` and other files in `GroupTheory/Perm/*`.
+-/
+
+universe u v
+
+open Equiv Function Fintype Finset
+
+open BigOperators
+
+variable {α : Type u} {β : Type v}
+
+-- An example on how to determine the order of an element of a finite group.
+example : orderOf (-1 : ℤˣ) = 2 :=
+  orderOf_eq_prime (Int.units_sq _) (by decide)
+
+namespace Equiv.Perm
+
+section Conjugation
+
+variable [DecidableEq α] [Fintype α] {σ τ : Perm α}
+
+theorem isConj_of_support_equiv
+    (f : { x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
+    (hf : ∀ (x : α) (hx : x ∈ (σ.support : Set α)),
+      (f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
+    IsConj σ τ := by
+  refine' isConj_iff.2 ⟨Equiv.extendSubtype f, _⟩
+  rw [mul_inv_eq_iff_eq_mul]
+  ext x
+  simp only [Perm.mul_apply]
+  by_cases hx : x ∈ σ.support
+  · rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
+    · exact hf x (Finset.mem_coe.2 hx)
+  · rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
+      Classical.not_not.1 ((not_congr mem_support).mp hx)]
+#align equiv.perm.is_conj_of_support_equiv Equiv.Perm.isConj_of_support_equiv
+
+end Conjugation
+
+
+
+theorem perm_inv_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α}
+    (hy : y ∈ s) : f⁻¹ y ∈ s := by
+  have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
+    Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
+      (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
+  obtain ⟨y2, hy2, heq⟩ := h0 y hy
+  convert hy2
+  rw [heq]
+  simp only [inv_apply_self]
+#align equiv.perm.perm_inv_on_of_perm_on_finset Equiv.Perm.perm_inv_on_of_perm_on_finset
+
+theorem perm_inv_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) :
+    Set.MapsTo (f⁻¹ : _) s s := by
+  cases nonempty_fintype s;
+    exact fun x hx =>
+      Set.mem_toFinset.mp <|
+        perm_inv_on_of_perm_on_finset
+          (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
+          (Set.mem_toFinset.mpr hx)
+#align equiv.perm.perm_inv_maps_to_of_maps_to Equiv.Perm.perm_inv_mapsTo_of_mapsTo
+
+@[simp]
+theorem perm_inv_mapsTo_iff_mapsTo {f : Perm α} {s : Set α} [Finite s] :
+    Set.MapsTo (f⁻¹ : _) s s ↔ Set.MapsTo f s s :=
+  ⟨perm_inv_mapsTo_of_mapsTo f⁻¹, perm_inv_mapsTo_of_mapsTo f⟩
+#align equiv.perm.perm_inv_maps_to_iff_maps_to Equiv.Perm.perm_inv_mapsTo_iff_mapsTo
+
+theorem perm_inv_on_of_perm_on_finite {f : Perm α} {p : α → Prop} [Finite { x // p x }]
+    (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x) :=
+  -- Porting note: relies heavily on the definitions of `Subtype` and `setOf` unfolding to their
+  -- underlying predicate.
+  have : Finite { x | p x } := ‹_›
+  perm_inv_mapsTo_of_mapsTo (s := {x | p x}) f h hx
+#align equiv.perm.perm_inv_on_of_perm_on_finite Equiv.Perm.perm_inv_on_of_perm_on_finite
+
+/-- If the permutation `f` maps `{x // p x}` into itself, then this returns the permutation
+  on `{x // p x}` induced by `f`. Note that the `h` hypothesis is weaker than for
+  `Equiv.Perm.subtypePerm`. -/
+abbrev subtypePermOfFintype (f : Perm α) {p : α → Prop} [Finite { x // p x }]
+    (h : ∀ x, p x → p (f x)) : Perm { x // p x } :=
+  f.subtypePerm fun x => ⟨h x, fun h₂ => f.inv_apply_self x ▸ perm_inv_on_of_perm_on_finite h h₂⟩
+#align equiv.perm.subtype_perm_of_fintype Equiv.Perm.subtypePermOfFintype
+
+@[simp]
+theorem subtypePermOfFintype_apply (f : Perm α) {p : α → Prop} [Finite { x // p x }]
+    (h : ∀ x, p x → p (f x)) (x : { x // p x }) : subtypePermOfFintype f h x = ⟨f x, h x x.2⟩ :=
+  rfl
+#align equiv.perm.subtype_perm_of_fintype_apply Equiv.Perm.subtypePermOfFintype_apply
+
+theorem subtypePermOfFintype_one (p : α → Prop) [Finite { x // p x }]
+    (h : ∀ x, p x → p ((1 : Perm α) x)) : @subtypePermOfFintype α 1 p _ h = 1 :=
+  rfl
+#align equiv.perm.subtype_perm_of_fintype_one Equiv.Perm.subtypePermOfFintype_one
+
+theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ : Perm (Sum m n)) :
+    Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl) ↔
+      Set.MapsTo σ (Set.range Sum.inr) (Set.range Sum.inr) := by
+  constructor <;>
+    ( intro h
+      classical
+        rw [← perm_inv_mapsTo_iff_mapsTo] at h
+        intro x
+        cases' hx : σ x with l r)
+  · rintro ⟨a, rfl⟩
+    obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
+    rw [← hx, σ.inv_apply_self] at hy
+    exact absurd hy Sum.inl_ne_inr
+  · rintro _; exact ⟨r, rfl⟩
+  · rintro _; exact ⟨l, rfl⟩
+  · rintro ⟨a, rfl⟩
+    obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
+    rw [← hx, σ.inv_apply_self] at hy
+    exact absurd hy Sum.inr_ne_inl
+#align equiv.perm.perm_maps_to_inl_iff_maps_to_inr Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr
+
+theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n]
+    {σ : Perm (Sum m n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
+    σ ∈ (sumCongrHom m n).range := by
+  classical
+    have h1 : ∀ x : Sum m n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
+      rintro x ⟨a, ha⟩
+      apply h
+      rw [← ha]
+      exact ⟨a, rfl⟩
+    have h3 : ∀ x : Sum m n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
+      rintro x ⟨b, hb⟩
+      apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
+      rw [← hb]
+      exact ⟨b, rfl⟩
+    let σ₁' := subtypePermOfFintype σ h1
+    let σ₂' := subtypePermOfFintype σ h3
+    let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
+    let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
+    rw [MonoidHom.mem_range, Prod.exists]
+    use σ₁, σ₂
+    rw [Perm.sumCongrHom_apply]
+    ext x
+    cases' x with a b
+    · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
+        apply_ofInjective_symm Sum.inl_injective]
+      rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
+      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+      erw [subtypePerm_apply]
+    · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
+        apply_ofInjective_symm Sum.inr_injective]
+      erw [subtypePerm_apply]
+      rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
+#align equiv.perm.mem_sum_congr_hom_range_of_perm_maps_to_inl Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl
+
+nonrec theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) :
+    orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=
+  haveI h : ∀ n : ℕ, (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1 := fun n => by
+    rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
+  Nat.dvd_antisymm hστ.commute.orderOf_mul_dvd_lcm
+    (Nat.lcm_dvd
+      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).1)
+      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).2))
+#align equiv.perm.disjoint.order_of Equiv.Perm.Disjoint.orderOf
+
+theorem Disjoint.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
+    {σ τ : Perm α} (h : Disjoint σ τ) : Disjoint (σ.extendDomain f) (τ.extendDomain f) := by
+  intro b
+  by_cases pb : p b
+  · refine' (h (f.symm ⟨b, pb⟩)).imp _ _ <;>
+      · intro h
+        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
+  · left
+    rw [extendDomain_apply_not_subtype _ _ pb]
+#align equiv.perm.disjoint.extend_domain Equiv.Perm.Disjoint.extendDomain
+
+theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
+    (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
+  classical
+    cases nonempty_fintype α
+    obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
+    obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
+    have hd1' := coe_inj.2 hd1.support_mul
+    have hd2' := coe_inj.2 hd2.support_mul
+    rw [coe_union] at *
+    have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
+    have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
+    refine' isConj_of_support_equiv _ _
+    · refine'
+          ((Equiv.Set.ofEq hd1').trans (Equiv.Set.union hd1''.le_bot)).trans
+            ((Equiv.sumCongr (subtypeEquiv f fun a => _) (subtypeEquiv g fun a => _)).trans
+              ((Equiv.Set.ofEq hd2').trans (Equiv.Set.union hd2''.le_bot)).symm) <;>
+      · simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
+          apply_eq_iff_eq]
+    · intro x hx
+      simp only [trans_apply, symm_trans_apply, Equiv.Set.ofEq_apply, Equiv.Set.ofEq_symm_apply,
+        Equiv.sumCongr_apply]
+      rw [hd1', Set.mem_union] at hx
+      cases' hx with hxσ hxτ
+      · rw [mem_coe, mem_support] at hxσ
+        rw [Set.union_apply_left hd1''.le_bot _, Set.union_apply_left hd1''.le_bot _]
+        simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
+          Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq]
+        · have h := (hd2 (f x)).resolve_left ?_
+          · rw [mul_apply, mul_apply] at h
+            rw [h, inv_apply_self, (hd1 x).resolve_left hxσ]
+          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
+        · rwa [Subtype.coe_mk, mem_coe, mem_support]
+        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
+            apply_mem_support, mem_support]
+      · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
+        rw [Set.union_apply_right hd1''.le_bot _, Set.union_apply_right hd1''.le_bot _]
+        simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
+          Set.union_symm_apply_right, Subtype.coe_mk, apply_eq_iff_eq]
+        · have h := (hd2 (g (τ x))).resolve_right ?_
+          · rw [mul_apply, mul_apply] at h
+            rw [inv_apply_self, h, (hd1 (τ x)).resolve_right hxτ]
+          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
+        · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
+        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
+            mem_coe, mem_support]
+#align equiv.perm.disjoint.is_conj_mul Equiv.Perm.Disjoint.isConj_mul
+
+
+variable [DecidableEq α]
+
+section Fintype
+
+variable [Fintype α]
+
+theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) :
+    (σ ^ n).support = σ.support := by
+  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
+  exact
+    le_antisymm (support_pow_le σ n)
+      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))
+#align equiv.perm.support_pow_coprime Equiv.Perm.support_pow_coprime
+
+end Fintype
+
+end Equiv.Perm
diff --git a/Mathlib/GroupTheory/Perm/Option.lean b/Mathlib/GroupTheory/Perm/Option.lean
index a2aab1f28aeb4..d4d2e3ca94bc4 100644
--- a/Mathlib/GroupTheory/Perm/Option.lean
+++ b/Mathlib/GroupTheory/Perm/Option.lean
@@ -3,7 +3,9 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
+import Mathlib.Data.Fintype.Option
 import Mathlib.Data.Fintype.Perm
+import Mathlib.Data.Fintype.Prod
 import Mathlib.GroupTheory.Perm.Sign
 import Mathlib.Logic.Equiv.Option
 
diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
index 4ba9e3feb3c41..554ada7fed4a5 100644
--- a/Mathlib/GroupTheory/Perm/Sign.lean
+++ b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -3,36 +3,35 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.GroupTheory.Perm.Support
-import Mathlib.GroupTheory.OrderOfElement
+
+import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Data.Finset.Fin
+import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Int.Order.Units
+import Mathlib.GroupTheory.Perm.Support
+import Mathlib.GroupTheory.Subgroup.Finite
+import Mathlib.Logic.Equiv.Fin
+import Mathlib.Tactic.NormNum.Ineq
 
 #align_import group_theory.perm.sign from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
 
 /-!
 # Sign of a permutation
 
-The main definition of this file is `Equiv.Perm.sign`, associating a `ℤˣ` sign with a
-permutation.
+The main definition of this file is `Equiv.Perm.sign`,
+associating a `ℤˣ` sign with a permutation.
 
-This file also contains miscellaneous lemmas about `Equiv.Perm` and `Equiv.swap`, building on top
-of those in `Data/Equiv/Basic` and other files in `GroupTheory/Perm/*`.
+Other lemmas have been moved to `Mathlib.GroupTheory.Perm.Fintype`
 
 -/
 
-
 universe u v
 
 open Equiv Function Fintype Finset
 
 open BigOperators
 
-variable {α : Type u} {β : Type v}
-
--- An example on how to determine the order of an element of a finite group.
-example : orderOf (-1 : ℤˣ) = 2 :=
-  orderOf_eq_prime (Int.units_sq _) (by decide)
+variable {α : Type u} [DecidableEq α] {β : Type v}
 
 namespace Equiv.Perm
 
@@ -41,7 +40,7 @@ namespace Equiv.Perm
 We use this to partition permutations in `Matrix.det_zero_of_row_eq`, such that each partition
 sums up to `0`.
 -/
-def modSwap [DecidableEq α] (i j : α) : Setoid (Perm α) :=
+def modSwap (i j : α) : Setoid (Perm α) :=
   ⟨fun σ τ => σ = τ ∨ σ = swap i j * τ, fun σ => Or.inl (refl σ), fun {σ τ} h =>
     Or.casesOn h (fun h => Or.inl h.symm) fun h => Or.inr (by rw [h, swap_mul_self_mul]),
     fun {σ τ υ} hστ hτυ => by
@@ -56,152 +55,6 @@ noncomputable instance {α : Type*} [Fintype α] [DecidableEq α] (i j : α) :
     DecidableRel (modSwap i j).r :=
   fun _ _ => Or.decidable
 
-theorem perm_inv_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α}
-    (hy : y ∈ s) : f⁻¹ y ∈ s := by
-  have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
-    Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
-      (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
-  obtain ⟨y2, hy2, heq⟩ := h0 y hy
-  convert hy2
-  rw [heq]
-  simp only [inv_apply_self]
-#align equiv.perm.perm_inv_on_of_perm_on_finset Equiv.Perm.perm_inv_on_of_perm_on_finset
-
-theorem perm_inv_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) :
-    Set.MapsTo (f⁻¹ : _) s s := by
-  cases nonempty_fintype s;
-    exact fun x hx =>
-      Set.mem_toFinset.mp <|
-        perm_inv_on_of_perm_on_finset
-          (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
-          (Set.mem_toFinset.mpr hx)
-#align equiv.perm.perm_inv_maps_to_of_maps_to Equiv.Perm.perm_inv_mapsTo_of_mapsTo
-
-@[simp]
-theorem perm_inv_mapsTo_iff_mapsTo {f : Perm α} {s : Set α} [Finite s] :
-    Set.MapsTo (f⁻¹ : _) s s ↔ Set.MapsTo f s s :=
-  ⟨perm_inv_mapsTo_of_mapsTo f⁻¹, perm_inv_mapsTo_of_mapsTo f⟩
-#align equiv.perm.perm_inv_maps_to_iff_maps_to Equiv.Perm.perm_inv_mapsTo_iff_mapsTo
-
-theorem perm_inv_on_of_perm_on_finite {f : Perm α} {p : α → Prop} [Finite { x // p x }]
-    (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x) :=
-  -- Porting note: relies heavily on the definitions of `Subtype` and `setOf` unfolding to their
-  -- underlying predicate.
-  have : Finite { x | p x } := ‹_›
-  perm_inv_mapsTo_of_mapsTo (s := {x | p x}) f h hx
-#align equiv.perm.perm_inv_on_of_perm_on_finite Equiv.Perm.perm_inv_on_of_perm_on_finite
-
-/-- If the permutation `f` maps `{x // p x}` into itself, then this returns the permutation
-  on `{x // p x}` induced by `f`. Note that the `h` hypothesis is weaker than for
-  `Equiv.Perm.subtypePerm`. -/
-abbrev subtypePermOfFintype (f : Perm α) {p : α → Prop} [Finite { x // p x }]
-    (h : ∀ x, p x → p (f x)) : Perm { x // p x } :=
-  f.subtypePerm fun x => ⟨h x, fun h₂ => f.inv_apply_self x ▸ perm_inv_on_of_perm_on_finite h h₂⟩
-#align equiv.perm.subtype_perm_of_fintype Equiv.Perm.subtypePermOfFintype
-
-@[simp]
-theorem subtypePermOfFintype_apply (f : Perm α) {p : α → Prop} [Finite { x // p x }]
-    (h : ∀ x, p x → p (f x)) (x : { x // p x }) : subtypePermOfFintype f h x = ⟨f x, h x x.2⟩ :=
-  rfl
-#align equiv.perm.subtype_perm_of_fintype_apply Equiv.Perm.subtypePermOfFintype_apply
-
-theorem subtypePermOfFintype_one (p : α → Prop) [Finite { x // p x }]
-    (h : ∀ x, p x → p ((1 : Perm α) x)) : @subtypePermOfFintype α 1 p _ h = 1 :=
-  rfl
-#align equiv.perm.subtype_perm_of_fintype_one Equiv.Perm.subtypePermOfFintype_one
-
-theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ : Perm (Sum m n)) :
-    Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl) ↔
-      Set.MapsTo σ (Set.range Sum.inr) (Set.range Sum.inr) := by
-  constructor <;>
-    ( intro h
-      classical
-        rw [← perm_inv_mapsTo_iff_mapsTo] at h
-        intro x
-        cases' hx : σ x with l r)
-  · rintro ⟨a, rfl⟩
-    obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
-    rw [← hx, σ.inv_apply_self] at hy
-    exact absurd hy Sum.inl_ne_inr
-  · rintro _; exact ⟨r, rfl⟩
-  · rintro _; exact ⟨l, rfl⟩
-  · rintro ⟨a, rfl⟩
-    obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
-    rw [← hx, σ.inv_apply_self] at hy
-    exact absurd hy Sum.inr_ne_inl
-#align equiv.perm.perm_maps_to_inl_iff_maps_to_inr Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr
-
-theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n]
-    {σ : Perm (Sum m n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
-    σ ∈ (sumCongrHom m n).range := by
-  classical
-    have h1 : ∀ x : Sum m n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
-      rintro x ⟨a, ha⟩
-      apply h
-      rw [← ha]
-      exact ⟨a, rfl⟩
-    have h3 : ∀ x : Sum m n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
-      rintro x ⟨b, hb⟩
-      apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
-      rw [← hb]
-      exact ⟨b, rfl⟩
-    let σ₁' := subtypePermOfFintype σ h1
-    let σ₂' := subtypePermOfFintype σ h3
-    let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
-    let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
-    rw [MonoidHom.mem_range, Prod.exists]
-    use σ₁, σ₂
-    rw [Perm.sumCongrHom_apply]
-    ext x
-    cases' x with a b
-    · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
-        apply_ofInjective_symm Sum.inl_injective]
-      rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
-      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [subtypePerm_apply]
-    · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
-        apply_ofInjective_symm Sum.inr_injective]
-      erw [subtypePerm_apply]
-      rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
-#align equiv.perm.mem_sum_congr_hom_range_of_perm_maps_to_inl Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl
-
-nonrec theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) :
-    orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=
-  haveI h : ∀ n : ℕ, (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1 := fun n => by
-    rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
-  Nat.dvd_antisymm hστ.commute.orderOf_mul_dvd_lcm
-    (Nat.lcm_dvd
-      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).1)
-      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).2))
-#align equiv.perm.disjoint.order_of Equiv.Perm.Disjoint.orderOf
-
-theorem Disjoint.extendDomain {α : Type*} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
-    {σ τ : Perm α} (h : Disjoint σ τ) : Disjoint (σ.extendDomain f) (τ.extendDomain f) := by
-  intro b
-  by_cases pb : p b
-  · refine' (h (f.symm ⟨b, pb⟩)).imp _ _ <;>
-      · intro h
-        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-  · left
-    rw [extendDomain_apply_not_subtype _ _ pb]
-#align equiv.perm.disjoint.extend_domain Equiv.Perm.Disjoint.extendDomain
-
-variable [DecidableEq α]
-
-section Fintype
-
-variable [Fintype α]
-
-theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) :
-    (σ ^ n).support = σ.support := by
-  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
-  exact
-    le_antisymm (support_pow_le σ n)
-      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))
-#align equiv.perm.support_pow_coprime Equiv.Perm.support_pow_coprime
-
-end Fintype
-
 /-- Given a list `l : List α` and a permutation `f : Perm α` such that the nonfixed points of `f`
   are in `l`, recursively factors `f` as a product of transpositions. -/
 def swapFactorsAux :
diff --git a/Mathlib/GroupTheory/Perm/Support.lean b/Mathlib/GroupTheory/Perm/Support.lean
index 7da05294e3383..87cff444a80b2 100644
--- a/Mathlib/GroupTheory/Perm/Support.lean
+++ b/Mathlib/GroupTheory/Perm/Support.lean
@@ -3,11 +3,12 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Aaron Anderson, Yakov Pechersky
 -/
-import Mathlib.Data.Finset.Card
-import Mathlib.Data.Fintype.Basic
+
+import Mathlib.Data.Fintype.Card
 import Mathlib.GroupTheory.Perm.Basic
 
 #align_import group_theory.perm.support from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
+
 /-!
 # support of a permutation
 
@@ -21,6 +22,11 @@ In the following, `f g : Equiv.Perm α`.
 * `Equiv.Perm.IsSwap`: `f = swap x y` for `x ≠ y`.
 * `Equiv.Perm.support`: the elements `x : α` that are not fixed by `f`.
 
+Assume `α` is a Fintype:
+* `Equiv.Perm.fixed_point_card_lt_of_ne_one f` says that `f` has
+  strictly less than `Fintype.card α - 1` fixed points, unless `f = 1`.
+  (Equivalently, `f.support` has at least 2 elements.)
+
 -/
 
 
@@ -665,3 +671,43 @@ theorem support_subtype_perm [DecidableEq α] {s : Finset α} (f : Perm α) (h)
 #align equiv.perm.support_subtype_perm Equiv.Perm.support_subtype_perm
 
 end Equiv.Perm
+
+section FixedPoints
+
+namespace Equiv.Perm
+/-!
+### Fixed points
+-/
+
+variable {α : Type*}
+
+theorem fixed_point_card_lt_of_ne_one [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
+    (filter (fun x => σ x = x) univ).card < Fintype.card α - 1 := by
+  rw [lt_tsub_iff_left, ← lt_tsub_iff_right, ← Finset.card_compl, Finset.compl_filter]
+  exact one_lt_card_support_of_ne_one h
+#align equiv.perm.fixed_point_card_lt_of_ne_one Equiv.Perm.fixed_point_card_lt_of_ne_one
+
+end Equiv.Perm
+
+end FixedPoints
+
+section Conjugation
+
+namespace Equiv.Perm
+
+variable {α : Type*} [Fintype α] [DecidableEq α] {σ τ : Perm α}
+
+@[simp]
+theorem support_conj : (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding := by
+  ext
+  simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne.def, Perm.mem_support,
+    Equiv.eq_symm_apply]
+  rfl
+#align equiv.perm.support_conj Equiv.Perm.support_conj
+
+theorem card_support_conj : (σ * τ * σ⁻¹).support.card = τ.support.card := by simp
+#align equiv.perm.card_support_conj Equiv.Perm.card_support_conj
+
+end Equiv.Perm
+
+end Conjugation
diff --git a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean
index fc9356256243f..8ede8f0827e8c 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean
@@ -40,6 +40,9 @@ alternating group permutation
 
 -/
 
+-- An example on how to determine the order of an element of a finite group.
+example : orderOf (-1 : ℤˣ) = 2 :=
+  orderOf_eq_prime (Int.units_sq _) (by decide)
 
 open Equiv Equiv.Perm Subgroup Fintype
 
diff --git a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
index 8d3201dec5da5..bf8758c3a2484 100644
--- a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
+++ b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Alternating.Basic
 import Mathlib.LinearAlgebra.Multilinear.TensorProduct
-
+import Mathlib.GroupTheory.GroupAction.Quotient
 /-!
 # Exterior product of alternating maps