refactor(data/finset/noncomm_prod): Use set.pairwise (#16859)

Redefine the various `noncomm_prod`s using `set.pairwise`. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the trivial `i = j` case.

Author: YaelDillies

src/algebra/group/commute.lean

@@ -54,6 +54,12 @@ protected lemma symm {a b : S} (h : commute a b) : commute b a := eq.symm h
 protected theorem symm_iff {a b : S} : commute a b ↔ commute b a :=
 ⟨commute.symm, commute.symm⟩
 
+@[to_additive] instance : is_refl S commute := ⟨commute.refl⟩
+
+-- This instance is useful for `finset.noncomm_prod`
+@[to_additive] instance on_is_refl {f : G → S} : is_refl G (λ a b, commute (f a) (f b)) :=
+⟨λ _, commute.refl _⟩
+
 end has_mul
 
 section semigroup

src/analysis/normed_space/exponential.lean

@@ -452,18 +452,17 @@ end
 /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually
 commute then `exp 𝕂 (∑ i, f i) = ∏ i, exp 𝕂 (f i)`. -/
 lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → 𝔸)
-  (h : ∀ (i ∈ s) (j ∈ s), commute (f i) (f j)) :
+  (h : (s : set ι).pairwise $ λ i j, commute (f i) (f j)) :
   exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i))
-    (λ i hi j hj, (h i hi j hj).exp 𝕂) :=
+    (λ i hi j hj _, (h.of_refl hi hj).exp 𝕂) :=
 begin
   classical,
   induction s using finset.induction_on with a s ha ih,
   { simp },
   rw [finset.noncomm_prod_insert_of_not_mem _ _ _ _ ha, finset.sum_insert ha,
-      exp_add_of_commute, ih],
-  refine commute.sum_right _ _ _ _,
-  intros i hi,
-  exact h _ (finset.mem_insert_self _ _) _ (finset.mem_insert_of_mem hi),
+      exp_add_of_commute, ih (h.mono $ finset.subset_insert _ _)],
+  refine commute.sum_right _ _ _ (λ i hi, _),
+  exact h.of_refl (finset.mem_insert_self _ _) (finset.mem_insert_of_mem hi),
 end
 
 lemma exp_nsmul (n : ℕ) (x : 𝔸) :
@@ -591,7 +590,7 @@ lemma exp_sum {ι} (s : finset ι) (f : ι → 𝔸) :
   exp 𝕂 (∑ i in s, f i) = ∏ i in s, exp 𝕂 (f i) :=
 begin
   rw [exp_sum_of_commute, finset.noncomm_prod_eq_prod],
-  exact λ i hi j hj, commute.all _ _,
+  exact λ i hi j hj _, commute.all _ _,
 end
 
 end comm_algebra

src/analysis/normed_space/matrix_exponential.lean

@@ -149,9 +149,9 @@ begin
 end
 
 lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → matrix m m 𝔸)
-  (h : ∀ (i ∈ s) (j ∈ s), commute (f i) (f j)) :
+  (h : (s : set ι).pairwise $ λ i j, commute (f i) (f j)) :
   exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i))
-    (λ i hi j hj, (h i hi j hj).exp 𝕂) :=
+    (λ i hi j hj _, (h.of_refl hi hj).exp 𝕂) :=
 begin
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,

src/data/finset/basic.lean

@@ -2025,6 +2025,9 @@ def to_finset (l : list α) : finset α := multiset.to_finset l
 lemma to_finset_eq (n : nodup l) : @finset.mk α l n = l.to_finset := multiset.to_finset_eq n
 
 @[simp] lemma mem_to_finset : a ∈ l.to_finset ↔ a ∈ l := mem_dedup
+@[simp, norm_cast] lemma coe_to_finset (l : list α) : (l.to_finset : set α) = {a | a ∈ l} :=
+set.ext $ λ _, list.mem_to_finset
+
 @[simp] lemma to_finset_nil : to_finset (@nil α) = ∅ := rfl
 
 @[simp] lemma to_finset_cons : to_finset (a :: l) = insert a (to_finset l) :=