refactor(group_theory/perm/*): disjoint and support in own file (#7450)

The group_theory/perm/sign file was getting large and too broad in scope. This refactor pulls out `perm.support`, `perm.is_swap`, and `perm.disjoint` into a separate file.

A simpler version of #7118.

src/group_theory/perm/cycle_type.lean

@@ -43,7 +43,7 @@ begin
   { exact ⟨false.elim, λ h, h4 (h 1)⟩ },
   { rw [mem_cons_iff, list.prod_cons,
         ih (λ σ hσ, h1 σ (list.mem_cons_of_mem τ hσ)) (pairwise_of_pairwise_cons h2)],
-    have key := disjoint_prod_list_of_disjoint (pairwise_cons.mp h2).1,
+    have key := disjoint_prod_right _ (pairwise_cons.mp h2).1,
     cases key a,
     { simp_rw [key.mul_comm, commute.mul_pow key.mul_comm.symm, mul_apply,
         pow_apply_eq_self_of_apply_eq_self h, or_iff_right_iff_imp],
@@ -252,7 +252,7 @@ begin
         multiset.map_cons, hσ', cons_inj_right, coe_map] at hπ,
       rw [hπ, cycle_type_eq (l.erase σ') rfl (λ f hf, hl1 f (list.erase_subset _ _ hf))
         (list.pairwise_of_sublist (list.erase_sublist _ _) hl2)] },
-    { refine disjoint_prod_list_of_disjoint (λ g hg, list.rel_of_pairwise_cons _ hg),
+    { refine disjoint_prod_right _ (λ g hg, list.rel_of_pairwise_cons _ hg),
       refine (list.perm.pairwise_iff _ (list.perm_cons_erase hσ'l).symm).2 hl2,
       exact (λ _ _, disjoint.symm) } }
 end

src/group_theory/perm/cycles.lean

@@ -236,8 +236,8 @@ calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
       card_support_swap hx.1.symm], refl }
   else
     have h : card (support (swap x (f x) * f)) + 1 = card (support f),
-      by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq h1,
-        card_insert_of_not_mem (not_mem_erase _ _)],
+      by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
+        card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase],
     have wf : card (support (swap x (f x) * f)) < card (support f),
       from card_support_swap_mul hx.1,
     by { rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h],
@@ -462,7 +462,7 @@ begin
   { intros h1 h2,
     rw list.prod_cons,
     exact induction_disjoint σ l.prod
-      (disjoint_prod_list_of_disjoint (list.pairwise_cons.mp h2).1)
+      (disjoint_prod_right _ (list.pairwise_cons.mp h2).1)
       (h1 _ (list.mem_cons_self _ _))
       (base_cycles σ (h1 σ (l.mem_cons_self σ)))
       (ih (λ τ hτ, h1 τ (list.mem_cons_of_mem σ hτ)) (list.pairwise_of_pairwise_cons h2)) },