chore: golf proofs involving permutations (#31389)

This reduces the diff of #27433.

Author: YaelDillies

Mathlib/Algebra/Group/End.lean

@@ -367,8 +367,8 @@ variable {p : α → Prop} {f : Perm α}
 def subtypePerm (f : Perm α) (h : ∀ x, p (f x) ↔ p x) : Perm { x // p x } where
   toFun := fun x => ⟨f x, (h _).2 x.2⟩
   invFun := fun x => ⟨f⁻¹ x, (h (f⁻¹ x)).1 <| by simpa using x.2⟩
-  left_inv _ := by simp only [Perm.inv_apply_self, Subtype.coe_eta]
-  right_inv _ := by simp only [Perm.apply_inv_self, Subtype.coe_eta]
+  left_inv _ := by simp
+  right_inv _ := by simp
 
 @[simp]
 theorem subtypePerm_apply (f : Perm α) (h : ∀ x, p (f x) ↔ p x) (x : { x // p x }) :
@@ -386,7 +386,7 @@ theorem subtypePerm_mul (f g : Perm α) (hf hg) :
   rfl
 
 private theorem inv_aux : (∀ x, p (f x) ↔ p x) ↔ ∀ x, p (f⁻¹ x) ↔ p x :=
-  f⁻¹.surjective.forall.trans <| by simp_rw [f.apply_inv_self, Iff.comm]
+  f⁻¹.surjective.forall.trans <| by simp [Iff.comm]
 
 /-- See `Equiv.Perm.inv_subtypePerm`. -/
 theorem subtypePerm_inv (f : Perm α) (hf) :
@@ -519,12 +519,10 @@ theorem swap_mul_self (i j : α) : swap i j * swap i j = 1 :=
 
 theorem swap_mul_eq_mul_swap (f : Perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
   Equiv.ext fun z => by
-    simp only [Perm.mul_apply, swap_apply_def]
-    split_ifs <;>
-      simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, not_true]
+    simp only [Perm.mul_apply, swap_apply_def]; split_ifs <;> simp_all [Perm.eq_inv_iff_eq]
 
 theorem mul_swap_eq_swap_mul (f : Perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f := by
-  rw [swap_mul_eq_mul_swap, Perm.inv_apply_self, Perm.inv_apply_self]
+  simp [swap_mul_eq_mul_swap]
 
 theorem swap_apply_apply (f : Perm α) (x y : α) : swap (f x) (f y) = f * swap x y * f⁻¹ := by
   rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]

Mathlib/Algebra/Order/Rearrangement.lean

@@ -170,26 +170,25 @@ theorem MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff (hfg : MonovaryOn f g s)
     (hσ : {x | σ x ≠ x} ⊆ s) :
     ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ σ) s := by
   classical
-  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm ?_⟩
-  · rw [MonovaryOn] at h
-    push_neg at h
-    obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
-    set τ : Perm ι := (Equiv.swap x y).trans σ
-    have hτs : {x | τ x ≠ x} ⊆ s := by
-      refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
-      obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
-    refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
-    obtain rfl | hxy := eq_or_ne x y
-    · cases lt_irrefl _ hfxy
-    simp only [τ, ← s.sum_erase_add _ hx,
-      ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
-      add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
-    refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
-      (smul_add_smul_lt_smul_add_smul hfxy hgxy)
-    simp_rw [mem_erase] at hz
-    rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
-  · convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
-    simp_rw [Function.comp_apply, apply_inv_self]
+  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
+    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ)⟩
+  rw [MonovaryOn] at h
+  push_neg at h
+  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
+  set τ : Perm ι := (Equiv.swap x y).trans σ
+  have hτs : {x | τ x ≠ x} ⊆ s := by
+    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
+    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
+  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
+  obtain rfl | hxy := eq_or_ne x y
+  · cases lt_irrefl _ hfxy
+  simp only [τ, ← s.sum_erase_add _ hx,
+    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
+    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
+  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
+    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
+  simp_rw [mem_erase] at hz
+  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
 
 /-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
 `g`, which antivary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`

Mathlib/Data/Fintype/Perm.lean

@@ -113,10 +113,9 @@ theorem nodup_permsOfList : ∀ {l : List α}, l.Nodup → (permsOfList l).Nodup
     · intro f hf₁ hf₂
       let ⟨x, hx, hx'⟩ := List.mem_flatMap.1 hf₂
       let ⟨g, hg⟩ := List.mem_map.1 hx'
-      have hgxa : g⁻¹ x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
-      have hxa : x ≠ a := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
-      exact (List.nodup_cons.1 hl).1 <|
-          hgxa ▸ mem_of_mem_permsOfList hg.1 (by rwa [apply_inv_self, hgxa])
+      obtain rfl : g⁻¹ x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
+      have hxa : x ≠ g⁻¹ x := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
+      exact (List.nodup_cons.1 hl).1 <| mem_of_mem_permsOfList hg.1 (by simpa using hxa)
 
 /-- Given a finset, produce the finset of all permutations of its elements. -/
 def permsOfFinset (s : Finset α) : Finset (Perm α) :=

Mathlib/GroupTheory/Perm/Centralizer.lean

@@ -167,8 +167,7 @@ theorem coe_toPermHom (k : centralizer {g}) (c : g.cycleFactorsFinset) :
 The equality is proved by `Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom'`. -/
 def range_toPermHom' : Subgroup (Perm g.cycleFactorsFinset) where
   carrier := {τ | ∀ c, #(τ c).val.support = #c.val.support}
-  one_mem' := by
-    simp only [Set.mem_setOf_eq, coe_one, id_eq, imp_true_iff]
+  one_mem' := by simp
   mul_mem' hσ hτ := by
     simp only [Subtype.forall, Set.mem_setOf_eq, coe_mul, Function.comp_apply]
     simp only [Subtype.forall, Set.mem_setOf_eq] at hσ hτ
@@ -177,9 +176,8 @@ def range_toPermHom' : Subgroup (Perm g.cycleFactorsFinset) where
   inv_mem' hσ := by
     simp only [Subtype.forall, Set.mem_setOf_eq] at hσ ⊢
     intro c hc
-    rw [← hσ]
-    · simp only [Finset.coe_mem, Subtype.coe_eta, apply_inv_self]
-    · simp only [Finset.coe_mem]
+    rw [← hσ _ (by simp)]
+    simp
 
 variable {g} in
 theorem mem_range_toPermHom'_iff {τ : Perm g.cycleFactorsFinset} :

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -61,7 +61,7 @@ protected theorem _root_.Eq.sameCycle (h : x = y) (f : Perm α) : f.SameCycle x
 
 @[symm]
 theorem SameCycle.symm : SameCycle f x y → SameCycle f y x := fun ⟨i, hi⟩ =>
-  ⟨-i, by rw [zpow_neg, ← hi, inv_apply_self]⟩
+  ⟨-i, by simp [zpow_neg, ← hi]⟩
 
 theorem sameCycle_comm : SameCycle f x y ↔ SameCycle f y x :=
   ⟨SameCycle.symm, SameCycle.symm⟩
@@ -250,9 +250,8 @@ theorem isCycle_inv : IsCycle f⁻¹ ↔ IsCycle f :=
 
 theorem IsCycle.conj : IsCycle f → IsCycle (g * f * g⁻¹) := by
   rintro ⟨x, hx, h⟩
-  refine ⟨g x, by simp [coe_mul, inv_apply_self, hx], fun y hy => ?_⟩
-  rw [← apply_inv_self g y]
-  exact (h <| eq_inv_iff_eq.not.2 hy).conj
+  refine ⟨g x, by simp [coe_mul, hx], fun y hy => ?_⟩
+  simpa using (h <| eq_inv_iff_eq.not.2 hy).conj (g := g)
 
 protected theorem IsCycle.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
     IsCycle g → IsCycle (g.extendDomain f) := by
@@ -366,48 +365,38 @@ theorem isCycle_swap_mul_aux₁ {α : Type*} [DecidableEq α] :
   | zero => exact fun _ h => ⟨0, h⟩
   | succ n hn =>
     intro b x f hb h
-    exact if hfbx : f x = b then ⟨0, hfbx⟩
-      else
-        have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
-        have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b := by
-          rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne, ←
-            f.injective.eq_iff, apply_inv_self]
-          exact this.1
-        let ⟨i, hi⟩ := hn hb' (f.injective <| by
-          rw [apply_inv_self]; rwa [pow_succ', mul_apply] at h)
-        ⟨i + 1, by
-          rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
-            swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]⟩
+    obtain hfbx | hfbx := eq_or_ne (f x) b
+    · exact ⟨0, hfbx⟩
+    have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
+    have hb' : (swap x (f x) * f) (f.symm b) ≠ f.symm b := by
+      simpa [swap_apply_of_ne_of_ne this.2 hfbx.symm, eq_symm_apply] using this.1
+    obtain ⟨i, hi⟩ := hn hb' <| f.injective <| by simpa [pow_succ'] using h
+    refine ⟨i + 1, ?_⟩
+    rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
+      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]
 
 theorem isCycle_swap_mul_aux₂ {α : Type*} [DecidableEq α] :
-    ∀ (n : ℤ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
-      ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b := by
-  intro n
-  cases n with
-  | ofNat n => exact isCycle_swap_mul_aux₁ n
-  | negSucc n =>
-    intro b x f hb h
-    exact if hfbx' : f x = b then ⟨0, hfbx'⟩
-      else
-        have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
-        have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b := by
-          rw [mul_apply, swap_apply_def]
-          split_ifs <;>
-            simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc, Ne, Perm.apply_inv_self] at *
-              <;> tauto
-        let ⟨i, hi⟩ :=
-          isCycle_swap_mul_aux₁ n hb
-            (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b by
-              rw [← zpow_natCast, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc,
-                ← inv_pow, pow_succ, mul_assoc, mul_assoc, inv_mul_cancel, mul_one, zpow_natCast,
-                ← pow_succ', ← pow_succ])
-        have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x := by
-          rw [mul_apply, inv_apply_self, swap_apply_left]
-        ⟨-i, by
-          rw [← add_sub_cancel_right i 1, neg_sub, sub_eq_add_neg, zpow_add, zpow_one, zpow_neg,
-            ← inv_zpow, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x,
-            zpow_add, zpow_one, mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self,
-            swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx')]⟩
+    ∀ (n : ℤ) {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b →
+      ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
+  | (n : ℕ), _, _, _, hb, h => isCycle_swap_mul_aux₁ n hb h
+  | .negSucc n, b, x, f, hb, h => by
+    obtain hfxb | hfxb := eq_or_ne (f x) b
+    · exact ⟨0, hfxb⟩
+    obtain ⟨hfb, hbx⟩ : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
+    replace hb : (swap x (f.symm x) * f⁻¹) (f.symm b) ≠ f.symm b := by
+      rw [mul_apply, swap_apply_def]
+      split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at * <;> tauto
+    obtain ⟨i, hi⟩ := isCycle_swap_mul_aux₁ n hb <| by
+      rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply] using h
+    refine ⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩
+    convert hi using 1
+    · rw [zpow_neg, ← inv_zpow, ← mul_apply, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul]
+      simp [swap_comm _ x, ← mul_apply, -coe_mul, ← inv_def, ← inv_def, mul_assoc _ f⁻¹,
+        ← mul_zpow_mul, mul_assoc _ _ f]
+      simp
+    · refine swap_apply_of_ne_of_ne ?_ ?_
+      · simpa [eq_comm, Perm.eq_inv_iff_eq, Perm.inv_eq_iff_eq] using hfxb
+      · simpa [eq_comm, eq_symm_apply, symm_apply_eq]
 
 theorem IsCycle.eq_swap_of_apply_apply_eq_self {α : Type*} [DecidableEq α] {f : Perm α}
     (hf : IsCycle f) {x : α} (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
@@ -429,15 +418,11 @@ theorem IsCycle.eq_swap_of_apply_apply_eq_self {α : Type*} [DecidableEq α] {f
           tauto
 
 theorem IsCycle.swap_mul {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α}
-    (hx : f x ≠ x) (hffx : f (f x) ≠ x) : IsCycle (swap x (f x) * f) :=
-  ⟨f x, by simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, hx],
-    fun y hy =>
-    let ⟨i, hi⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
-    have hi : (f ^ (i - 1)) (f x) = y :=
-      calc
-        (f ^ (i - 1) : Perm α) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ) : Perm α) x := by simp
-        _ = y := by rwa [← zpow_add, sub_add_cancel]
-    isCycle_swap_mul_aux₂ (i - 1) hy hi⟩
+    (hx : f x ≠ x) (hffx : f (f x) ≠ x) : IsCycle (swap x (f x) * f) := by
+  refine ⟨f x, ?_, fun y hy ↦ ?_⟩
+  · simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, hx]
+  obtain ⟨i, rfl⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
+  exact isCycle_swap_mul_aux₂ (i - 1) hy (by simp [← mul_apply, -coe_mul, ← zpow_add_one])
 
 theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ #f.support :=
   let ⟨x, hx⟩ := hf
@@ -609,7 +594,7 @@ theorem IsCycle.pow_eq_pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {a b :
       rw [hf.pow_eq_one_iff]
       by_cases hfa : (f ^ a) x ∈ f.support
       · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
-        simp only [pow_sub _ hab, Equiv.Perm.coe_mul, Function.comp_apply, inv_apply_self, ← hx']
+        simp [pow_sub _ hab, ← hx']
       · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
         simp only [zpow_one, zpow_natCast] at h
         rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
@@ -660,12 +645,8 @@ theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
     IsConj σ τ ↔ #σ.support = #τ.support where
   mp h := by
     obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
-    refine Finset.card_bij (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab)
-        fun b hb ↦ ⟨π⁻¹ b, ?_, π.apply_inv_self b⟩
-    · simp [mem_support.1 ha]
-    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]
+    exact Finset.card_bij (fun a _ => π a) (fun _ ha => by simpa using ha)
+      (fun _ _ _ _ ab => π.injective ab) fun b hb ↦ ⟨π⁻¹ b, by simpa using hb, π.apply_symm_apply b⟩
   mpr := hσ.isConj hτ
 
 end Conjugation
@@ -705,8 +686,8 @@ alias ⟨IsCycleOn.of_inv, IsCycleOn.inv⟩ := isCycleOn_inv
 
 theorem IsCycleOn.conj (h : f.IsCycleOn s) : (g * f * g⁻¹).IsCycleOn ((g : Perm α) '' s) :=
   ⟨(g.bijOn_image.comp h.1).comp g.bijOn_symm_image, fun x hx y hy => by
-    rw [← preimage_inv] at hx hy
-    convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]⟩
+    rw [Equiv.image_eq_preimage_symm] at hx hy
+    convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> simp⟩
 
 theorem isCycleOn_swap [DecidableEq α] (hab : a ≠ b) : (swap a b).IsCycleOn {a, b} :=
   ⟨bijOn_swap (by simp) (by simp), fun x hx y hy => by
@@ -738,9 +719,7 @@ theorem isCycle_iff_exists_isCycleOn :
     exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩
 
 theorem IsCycleOn.apply_mem_iff (hf : f.IsCycleOn s) : f x ∈ s ↔ x ∈ s :=
-  ⟨fun hx => by
-    convert hf.1.perm_inv.1 hx
-    rw [inv_apply_self], fun hx => hf.1.mapsTo hx⟩
+  ⟨fun hx => by simpa using hf.1.perm_inv.1 hx, fun hx => hf.1.mapsTo hx⟩
 
 /-- Note that the identity satisfies `IsCycleOn` for any subsingleton set, but not `IsCycle`. -/
 theorem IsCycleOn.isCycle_subtypePerm (hf : f.IsCycleOn s) (hs : s.Nontrivial) :

Mathlib/GroupTheory/Perm/Cycle/Factors.lean

@@ -397,30 +397,20 @@ where
       ⟨cycleOf f x :: m, by
         obtain ⟨hm₁, hm₂, hm₃⟩ := hm
         rw [hfg hx] at hm₁ ⊢
-        constructor
-        · rw [List.prod_cons, hm₁]
-          simp
-        · exact
-            ⟨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 hgy =>
-                    have hxy : SameCycle g x y :=
-                      Classical.not_not.1 (mt cycleOf_apply_of_not_sameCycle hgy)
-                    have hg'm : (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 ((hg'm.pairwise_iff Disjoint.symm).2 hm₃)).1
-                    by_cases id fun hg'y : g' y ≠ y =>
-                      (disjoint_prod_right _ this y).resolve_right <| by
-                        have hsc : SameCycle g⁻¹ x (g y) := by
-                          rwa [sameCycle_inv, sameCycle_apply_right]
-                        rw [disjoint_prod_perm hm₃ hg'm.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₃⟩⟩⟩
+        rw [List.pairwise_cons]
+        refine ⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩
+        · simp [List.prod_cons, hm₁]
+        · exact ((List.mem_cons).1 hg').elim (fun hg' => hg'.symm ▸ isCycle_cycleOf _ hx) (hm₂ g')
+        by_contra!
+        obtain ⟨hgy, hg'y⟩ := this
+        have hxy : SameCycle g x y := not_imp_comm.1 cycleOf_apply_of_not_sameCycle hgy
+        have hg'm : g' :: m.erase g' ~ m := List.cons_perm_iff_perm_erase.2 ⟨hg', .refl _⟩
+        have : ∀ h ∈ m.erase g', Disjoint g' h :=
+          (List.pairwise_cons.1 ((hg'm.pairwise_iff Disjoint.symm).2 hm₃)).1
+        refine hg'y <| (disjoint_prod_right _ this y).resolve_right ?_
+        have hsc : SameCycle g⁻¹ x (g y) := by rwa [sameCycle_inv, sameCycle_apply_right]
+        rw [disjoint_prod_perm hm₃ hg'm.symm, List.prod_cons, ← eq_inv_mul_iff_mul_eq] at hm₁
+        simpa [hm₁, cycleOf_inv, hsc.cycleOf_apply, Perm.eq_inv_iff_eq, eq_comm] using hg'y⟩
 
 theorem mem_list_cycles_iff {α : Type*} [Finite α] {l : List (Perm α)}
     (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) {σ : Perm α} :
@@ -691,9 +681,8 @@ theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cy
   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]
+  rw [mul_apply, ← h.right _ (by simpa [Perm.eq_inv_iff_eq])]
+  simp
 
 /-- 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)
@@ -749,11 +738,7 @@ theorem mem_cycleFactorsFinset_conj (g k c : Perm α) :
   intro hc a ha
   simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
   apply hc
-  rw [mem_support] at ha ⊢
-  contrapose! ha
-  simp only [mul_smul, ← Perm.smul_def] at ha ⊢
-  rw [ha]
-  simp only [Perm.smul_def, apply_inv_self]
+  simpa [inv_def, eq_symm_apply] using ha
 
 /-- If a permutation commutes with every cycle of `g`, then it commutes with `g`