From 2414ba09683d020daab208e4a9c29f15772910fa Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 27 Feb 2024 06:49:35 +0000
Subject: [PATCH] chore(GroupTheory/Perm): drop `DecidableEq`, `Fintype` ->
 `Finite` (#10917)

---
 Mathlib/GroupTheory/Perm/Cycle/Basic.lean | 48 ++++++++++-------------
 Mathlib/GroupTheory/Perm/Sign.lean        | 28 ++++++-------
 2 files changed, 34 insertions(+), 42 deletions(-)

diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
index e25e4a5d2154e..cdff4bdb51f07 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -1218,12 +1218,10 @@ end CycleOf
 ### `cycleFactors`
 -/
 
-variable [DecidableEq α]
-
 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 [Fintype α] :
+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
@@ -1325,7 +1323,7 @@ def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
 
 /-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
   without a linear order. -/
-def truncCycleFactors [Fintype α] (f : Perm α) :
+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 _)
@@ -1333,7 +1331,7 @@ def truncCycleFactors [Fintype α] (f : Perm α) :
 
 section CycleFactorsFinset
 
-variable [Fintype α] (f : Perm α)
+variable [DecidableEq α] [Fintype α] (f : Perm α)
 
 /-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
 -/
@@ -1547,7 +1545,7 @@ theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (ba
         (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 [Fintype α] {f g : Perm α}
+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'
@@ -1607,7 +1605,7 @@ theorem closure_isCycle : closure { σ : Perm β | IsCycle σ } = ⊤ := by
       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 [Fintype α]
+variable [DecidableEq α] [Fintype α]
 
 theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = ⊤) (x : α) :
     closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤ := by
@@ -1692,15 +1690,14 @@ end Generation
 
 section
 
-variable [Fintype α] {σ τ : Perm α}
-
 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⟩)) :
+    (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]
@@ -1762,7 +1759,7 @@ theorem card_support_conj : (σ * τ * σ⁻¹).support.card = τ.support.card :
 
 end
 
-theorem Disjoint.isConj_mul {α : Type*} [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
+theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
     (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
   classical
     cases nonempty_fintype α
@@ -1816,7 +1813,7 @@ section FixedPoints
 -/
 
 
-theorem fixed_point_card_lt_of_ne_one [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
+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
@@ -1866,9 +1863,8 @@ variable [DecidableEq α] [Fintype α]
 
 theorem _root_.Finset.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)⟩
+  refine ⟨s.toList.formPerm, ?_, fun x hx => by
+    simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)⟩
   convert s.nodup_toList.isCycleOn_formPerm
   simp
 #align finset.exists_cycle_on Finset.exists_cycleOn
@@ -1882,18 +1878,16 @@ variable {f : Perm α} {s : Set α}
 theorem _root_.Set.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
-    · refine'
-        ⟨hs'.toFinset.toList.formPerm, _, fun x hx => by
-          simpa using List.mem_of_formPerm_apply_ne _ _ hx⟩
-      convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
-      simp
-    haveI := hs.to_subtype
+  obtain hs' | hs' := s.finite_or_infinite
+  · refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
+      simpa using List.mem_of_formPerm_apply_ne _ _ hx⟩
+    convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
+    simp
+  · haveI := hs.to_subtype
     haveI := hs'.to_subtype
     obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
-    refine'
-      ⟨(Equiv.addRight 1).extendDomain f, _, fun x hx =>
-        of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
+    refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
+      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
     convert Int.addRight_one_isCycle.isCycleOn.extendDomain f
     rw [Set.image_comp, Equiv.image_eq_preimage]
     ext
diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
index d5bb51822585e..5564e17febe09 100644
--- a/Mathlib/GroupTheory/Perm/Sign.lean
+++ b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -322,8 +322,6 @@ def signBijAux {n : ℕ} (f : Perm (Fin n)) (a : Σ_ : Fin n, Fin n) : Σ_ : Fin
   if _ : f a.2 < f a.1 then ⟨f a.1, f a.2⟩ else ⟨f a.2, f a.1⟩
 #align equiv.perm.sign_bij_aux Equiv.Perm.signBijAux
 
--- porting note: Lean insists `ha` and `hb` are unused despite obvious uses
-set_option linter.unusedVariables false in
 theorem signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} :
     (finPairsLT n : Set (Σ _, Fin n)).InjOn (signBijAux f) := by
   rintro ⟨a₁, a₂⟩ ha ⟨b₁, b₂⟩ hb h
@@ -526,6 +524,19 @@ theorem signAux3_mul_and_swap [Finite α] (f g : Perm α) (s : Multiset α) (hs
     rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hexy]
 #align equiv.perm.sign_aux3_mul_and_swap Equiv.Perm.signAux3_mul_and_swap
 
+theorem signAux3_symm_trans_trans [Finite α] [DecidableEq β] [Finite β] (f : Perm α) (e : α ≃ β)
+    {s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
+    signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs := by
+  -- porting note: switched from term mode to tactic mode
+  induction' t, s using Quotient.inductionOn₂ with t s ht hs
+  show signAux2 _ _ = signAux2 _ _
+  rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩
+  rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _,
+    ← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]
+  exact congr_arg signAux
+    (Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
+#align equiv.perm.sign_aux3_symm_trans_trans Equiv.Perm.signAux3_symm_trans_trans
+
 /-- `SignType.sign` of a permutation returns the signature or parity of a permutation, `1` for even
 permutations, `-1` for odd permutations. It is the unique surjective group homomorphism from
 `Perm α` to the group with two elements.-/
@@ -581,19 +592,6 @@ theorem IsSwap.sign_eq {f : Perm α} (h : f.IsSwap) : sign f = -1 :=
   hxy.2.symm ▸ sign_swap hxy.1
 #align equiv.perm.is_swap.sign_eq Equiv.Perm.IsSwap.sign_eq
 
-theorem signAux3_symm_trans_trans [DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β)
-    {s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
-    signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs := by
-  -- porting note: switched from term mode to tactic mode
-  induction' t, s using Quotient.inductionOn₂ with t s ht hs
-  show signAux2 _ _ = signAux2 _ _
-  let n := equivFin β
-  rw [← signAux_eq_signAux2 _ _ n fun _ _ => ht _,
-    ← signAux_eq_signAux2 _ _ (e.trans n) fun _ _ => hs _]
-  exact congr_arg signAux
-    (Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
-#align equiv.perm.sign_aux3_symm_trans_trans Equiv.Perm.signAux3_symm_trans_trans
-
 @[simp]
 theorem sign_symm_trans_trans [DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β) :
     sign ((e.symm.trans f).trans e) = sign f :=