chore(Perm/List): golf, review API (#12302)

- add `mem_or_mem_of_zipWith_swap_prod_ne`, a version of `zipWith_swap_prod_support'` without any `Finset`s;
- move it and related lemmas up, use them to golf lemmas about `	formPerm`;
- convert explicit -> implicit arguments here and there;
- `formPerm_reverse` doesn't need `Nodup`

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -1001,7 +1001,7 @@ variable [DecidableEq α] [Fintype α]
 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)⟩
+    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
@@ -1017,7 +1017,7 @@ theorem Countable.exists_cycleOn (hs : s.Countable) :
   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⟩
+      simpa using List.mem_of_formPerm_apply_ne hx⟩
     convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
     simp
   · haveI := hs.to_subtype

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

@@ -185,7 +185,7 @@ theorem formPerm_apply_mem_eq_next (s : Cycle α) (h : Nodup s) (x : α) (hx : x
 nonrec theorem formPerm_reverse (s : Cycle α) (h : Nodup s) :
     formPerm s.reverse (nodup_reverse_iff.mpr h) = (formPerm s h)⁻¹ := by
   induction s using Quot.inductionOn
-  simpa using formPerm_reverse _ h
+  simpa using formPerm_reverse _
 #align cycle.form_perm_reverse Cycle.formPerm_reverse
 
 nonrec theorem formPerm_eq_formPerm_iff {α : Type*} [DecidableEq α] {s s' : Cycle α} {hs : s.Nodup}

Mathlib/GroupTheory/Perm/List.lean

@@ -68,55 +68,73 @@ theorem formPerm_pair (x y : α) : formPerm [x, y] = swap x y :=
   rfl
 #align list.form_perm_pair List.formPerm_pair
 
-variable {l} {x : α}
+theorem mem_or_mem_of_zipWith_swap_prod_ne : ∀ {l l' : List α} {x : α},
+    (zipWith swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l'
+  | [], _, _ => by simp
+  | _, [], _ => by simp
+  | a::l, b::l', x => fun hx ↦
+    if h : (zipWith swap l l').prod x = x then
+      (eq_or_eq_of_swap_apply_ne_self (by simpa [h] using hx)).imp
+        (by rintro rfl; exact .head _) (by rintro rfl; exact .head _)
+    else
+     (mem_or_mem_of_zipWith_swap_prod_ne h).imp (.tail _) (.tail _)
 
-theorem formPerm_apply_of_not_mem (x : α) (l : List α) (h : x ∉ l) : formPerm l x = x := by
-  cases' l with y l
-  · simp
-  induction' l with z l IH generalizing x y
-  · simp
-  · specialize IH x z (mt (mem_cons_of_mem y) h)
-    simp only [not_or, mem_cons] at h
-    simp [IH, swap_apply_of_ne_of_ne, h]
-#align list.form_perm_apply_of_not_mem List.formPerm_apply_of_not_mem
+theorem zipWith_swap_prod_support' (l l' : List α) :
+    { x | (zipWith swap l l').prod x ≠ x } ≤ l.toFinset ⊔ l'.toFinset := fun _ h ↦ by
+  simpa using mem_or_mem_of_zipWith_swap_prod_ne h
+#align list.zip_with_swap_prod_support' List.zipWith_swap_prod_support'
 
-theorem mem_of_formPerm_apply_ne (x : α) (l : List α) : l.formPerm x ≠ x → x ∈ l :=
-  not_imp_comm.2 <| List.formPerm_apply_of_not_mem _ _
+theorem zipWith_swap_prod_support [Fintype α] (l l' : List α) :
+    (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset := by
+  intro x hx
+  have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx
+  simpa using zipWith_swap_prod_support' _ _ hx'
+#align list.zip_with_swap_prod_support List.zipWith_swap_prod_support
+
+theorem support_formPerm_le' : { x | formPerm l x ≠ x } ≤ l.toFinset := by
+  refine' (zipWith_swap_prod_support' l l.tail).trans _
+  simpa [Finset.subset_iff] using tail_subset l
+#align list.support_form_perm_le' List.support_formPerm_le'
+
+theorem support_formPerm_le [Fintype α] : support (formPerm l) ≤ l.toFinset := by
+  intro x hx
+  have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
+  simpa using support_formPerm_le' _ hx'
+#align list.support_form_perm_le List.support_formPerm_le
+
+variable {l} {x : α}
+
+theorem mem_of_formPerm_apply_ne (h : l.formPerm x ≠ x) : x ∈ l := by
+  simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h
 #align list.mem_of_form_perm_apply_ne List.mem_of_formPerm_apply_ne
 
-theorem formPerm_apply_mem_of_mem (x : α) (l : List α) (h : x ∈ l) : formPerm l x ∈ l := by
+theorem formPerm_apply_of_not_mem (h : x ∉ l) : formPerm l x = x :=
+  not_imp_comm.1 mem_of_formPerm_apply_ne h
+#align list.form_perm_apply_of_not_mem List.formPerm_apply_of_not_mem
+
+theorem formPerm_apply_mem_of_mem (h : x ∈ l) : formPerm l x ∈ l := by
   cases' l with y l
   · simp at h
   induction' l with z l IH generalizing x y
   · simpa using h
   · by_cases hx : x ∈ z :: l
     · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
       split_ifs
-      · simp [IH _ _ hx]
+      · simp [IH _ hx]
       · simp
       · simp [*]
     · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
-      simp [formPerm_apply_of_not_mem _ _ hx, ← h]
+      simp [formPerm_apply_of_not_mem hx, ← h]
 #align list.form_perm_apply_mem_of_mem List.formPerm_apply_mem_of_mem
 
-theorem mem_of_formPerm_apply_mem (x : α) (l : List α) (h : l.formPerm x ∈ l) : x ∈ l := by
-  cases' l with y l
-  · simp at h
-  induction' l with z l IH generalizing x y
-  · simpa using h
-  · by_cases hx : (z :: l).formPerm x ∈ z :: l
-    · rw [List.formPerm_cons_cons, mul_apply, swap_apply_def] at h
-      split_ifs at h <;> aesop
-    · replace hx :=
-        (Function.Injective.eq_iff (Equiv.injective _)).mp (List.formPerm_apply_of_not_mem _ _ hx)
-      simp only [List.formPerm_cons_cons, hx, Equiv.Perm.coe_mul, Function.comp_apply,
-        List.mem_cons, swap_apply_def, ite_eq_left_iff] at h
-      simp only [List.mem_cons]
-      rcases h with h | h | h <;> split_ifs at h with h1 <;> try { aesop }
+theorem mem_of_formPerm_apply_mem (h : l.formPerm x ∈ l) : x ∈ l := by
+  contrapose h
+  rwa [formPerm_apply_of_not_mem h]
 #align list.mem_of_form_perm_apply_mem List.mem_of_formPerm_apply_mem
 
+@[simp]
 theorem formPerm_mem_iff_mem : l.formPerm x ∈ l ↔ x ∈ l :=
-  ⟨l.mem_of_formPerm_apply_mem x, l.formPerm_apply_mem_of_mem x⟩
+  ⟨l.mem_of_formPerm_apply_mem, l.formPerm_apply_mem_of_mem⟩
 #align list.form_perm_mem_iff_mem List.formPerm_mem_iff_mem
 
 @[simp]
@@ -141,7 +159,7 @@ theorem formPerm_apply_nthLe_length (x : α) (xs : List α) :
 #align list.form_perm_apply_nth_le_length List.formPerm_apply_nthLe_length
 
 theorem formPerm_apply_head (x y : α) (xs : List α) (h : Nodup (x :: y :: xs)) :
-    formPerm (x :: y :: xs) x = y := by simp [formPerm_apply_of_not_mem _ _ h.not_mem]
+    formPerm (x :: y :: xs) x = y := by simp [formPerm_apply_of_not_mem h.not_mem]
 #align list.form_perm_apply_head List.formPerm_apply_head
 
 set_option linter.deprecated false in
@@ -160,49 +178,6 @@ theorem formPerm_eq_head_iff_eq_getLast (x y : α) :
   Iff.trans (by rw [formPerm_apply_getLast]) (formPerm (y :: l)).injective.eq_iff
 #align list.form_perm_eq_head_iff_eq_last List.formPerm_eq_head_iff_eq_getLast
 
-theorem zipWith_swap_prod_support' (l l' : List α) :
-    { x | (zipWith swap l l').prod x ≠ x } ≤ l.toFinset ⊔ l'.toFinset := by
-  simp only [Set.sup_eq_union, Set.le_eq_subset]
-  induction' l with y l hl generalizing l'
-  · simp
-  · cases' l' with z l'
-    · simp
-    · intro x
-      simp only [Set.union_subset_iff, mem_cons, zipWith_cons_cons, foldr, prod_cons,
-        mul_apply]
-      intro hx
-      by_cases h : x ∈ { x | (zipWith swap l l').prod x ≠ x }
-      · specialize hl l' h
-        simp only [ge_iff_le, Finset.le_eq_subset, Finset.sup_eq_union, Finset.coe_union,
-          coe_toFinset, Set.mem_union, Set.mem_setOf_eq] at hl
-        refine' Or.elim hl (fun hm => _) fun hm => _ <;>
-          · simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, toFinset_cons,
-              mem_toFinset] at hm ⊢
-            simp [hm]
-      · simp only [not_not, Set.mem_setOf_eq] at h
-        simp only [h, Set.mem_setOf_eq] at hx
-        rw [swap_apply_ne_self_iff] at hx
-        rcases hx with ⟨hyz, rfl | rfl⟩ <;> simp
-#align list.zip_with_swap_prod_support' List.zipWith_swap_prod_support'
-
-theorem zipWith_swap_prod_support [Fintype α] (l l' : List α) :
-    (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset := by
-  intro x hx
-  have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx
-  simpa using zipWith_swap_prod_support' _ _ hx'
-#align list.zip_with_swap_prod_support List.zipWith_swap_prod_support
-
-theorem support_formPerm_le' : { x | formPerm l x ≠ x } ≤ l.toFinset := by
-  refine' (zipWith_swap_prod_support' l l.tail).trans _
-  simpa [Finset.subset_iff] using tail_subset l
-#align list.support_form_perm_le' List.support_formPerm_le'
-
-theorem support_formPerm_le [Fintype α] : support (formPerm l) ≤ l.toFinset := by
-  intro x hx
-  have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
-  simpa using support_formPerm_le' _ hx'
-#align list.support_form_perm_le List.support_formPerm_le
-
 set_option linter.deprecated false in
 theorem formPerm_apply_lt (xs : List α) (h : Nodup xs) (n : ℕ) (hn : n + 1 < xs.length) :
     formPerm xs (xs.nthLe n ((Nat.lt_succ_self n).trans hn)) = xs.nthLe (n + 1) hn := by
@@ -279,7 +254,7 @@ theorem formPerm_rotate_one (l : List α) (h : Nodup l) : formPerm (l.rotate 1)
   · obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
     rw [formPerm_apply_nthLe _ h', nthLe_rotate l, nthLe_rotate l, formPerm_apply_nthLe _ h]
     simp
-  · rw [formPerm_apply_of_not_mem _ _ hx, formPerm_apply_of_not_mem]
+  · rw [formPerm_apply_of_not_mem hx, formPerm_apply_of_not_mem]
     simpa using hx
 #align list.form_perm_rotate_one List.formPerm_rotate_one
 
@@ -298,33 +273,18 @@ theorem formPerm_eq_of_isRotated {l l' : List α} (hd : Nodup l) (h : l ~r l') :
   exact (formPerm_rotate l hd n).symm
 #align list.form_perm_eq_of_is_rotated List.formPerm_eq_of_isRotated
 
-set_option linter.deprecated false in
-theorem formPerm_reverse (l : List α) (h : Nodup l) : formPerm l.reverse = (formPerm l)⁻¹ := by
-  -- Let's show `formPerm l` is an inverse to `formPerm l.reverse`.
-  rw [eq_comm, inv_eq_iff_mul_eq_one]
-  ext x
-  -- We only have to check for `x ∈ l` that `formPerm l (formPerm l.reverse x)`
-  rw [mul_apply, one_apply]
-  cases' Classical.em (x ∈ l) with hx hx
-  · obtain ⟨k, hk, rfl⟩ := nthLe_of_mem (mem_reverse.mpr hx)
-    have h1 : l.length - 1 - k < l.length := by
-      rw [Nat.sub_sub, add_comm]
-      exact Nat.sub_lt_self (Nat.succ_pos _) (Nat.succ_le_of_lt (by simpa using hk))
-    have h2 : length l - 1 - (k + 1) % length (reverse l) < length l := by
-      rw [Nat.sub_sub, length_reverse];
-      exact Nat.sub_lt_self (by rw [add_comm]; exact Nat.succ_pos _)
-        (by rw [add_comm]; exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx)))
-    rw [formPerm_apply_nthLe l.reverse (nodup_reverse.mpr h), nthLe_reverse' _ _ _ h1,
-      nthLe_reverse' _ _ _ h2, formPerm_apply_nthLe _ h]
-    congr
-    rw [length_reverse] at *
-    rcases lt_or_eq_of_le (Nat.succ_le_of_lt hk) with h | h
-    · rw [Nat.mod_eq_of_lt h, ← Nat.sub_add_comm, Nat.succ_sub_succ_eq_sub,
-        Nat.mod_eq_of_lt h1]
-      exact (Nat.le_sub_iff_add_le (length_pos_of_mem hx)).2 (Nat.succ_le_of_lt h)
-    · rw [← h]; simp
-  · rw [formPerm_apply_of_not_mem x l.reverse, formPerm_apply_of_not_mem _ _ hx]
-    simpa using hx
+theorem formPerm_append_pair : ∀ (l : List α) (a b : α),
+    formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * swap a b
+  | [], _, _ => rfl
+  | [x], _, _ => rfl
+  | x::y::l, a, b => by
+    simpa [mul_assoc] using formPerm_append_pair (y::l) a b
+
+theorem formPerm_reverse : ∀ l : List α, formPerm l.reverse = (formPerm l)⁻¹
+  | [] => rfl
+  | [_] => rfl
+  | a::b::l => by
+    simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b::l)]
 #align list.form_perm_reverse List.formPerm_reverse
 
 theorem formPerm_pow_apply_get (l : List α) (h : Nodup l) (n k : ℕ) (hk : k < l.length) :

Mathlib/Logic/Equiv/Basic.lean

@@ -1647,6 +1647,10 @@ theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x
   simp (config := { contextual := true }) [swap_apply_def]
 #align equiv.swap_apply_of_ne_of_ne Equiv.swap_apply_of_ne_of_ne
 
+theorem eq_or_eq_of_swap_apply_ne_self {a b x : α} (h : swap a b x ≠ x) : x = a ∨ x = b := by
+  contrapose! h
+  exact swap_apply_of_ne_of_ne h.1 h.2
+
 @[simp]
 theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = Equiv.refl _ :=
   ext fun _ => swapCore_swapCore _ _ _