feat(data/list/pairwise): pairwise_of_forall_mem_list (#12968)

A relation holds pairwise on a list when it does on any two of its elements.

src/data/list/pairwise.lean

@@ -268,14 +268,19 @@ begin
         exact h x (mem_cons_of_mem _ hx) y (mem_cons_of_mem _ hy) } } }
 end
 
-lemma pairwise_of_reflexive_of_forall_ne {l : list α} {r : α → α → Prop}
-  (hr : reflexive r) (h : ∀ (a ∈ l) (b ∈ l), a ≠ b → r a b) : l.pairwise r :=
+lemma pairwise_of_forall_mem_list {l : list α} {r : α → α → Prop} (h : ∀ (a ∈ l) (b ∈ l), r a b) :
+  l.pairwise r :=
 begin
   classical,
-  refine pairwise_of_reflexive_on_dupl_of_forall_ne _ h,
-  exact λ _ _, hr _
+  refine pairwise_of_reflexive_on_dupl_of_forall_ne (λ a ha', _) (λ a ha b hb _, h a ha b hb),
+  have ha := list.one_le_count_iff_mem.1 ha'.le,
+  exact h a ha a ha
 end
 
+lemma pairwise_of_reflexive_of_forall_ne {l : list α} {r : α → α → Prop}
+  (hr : reflexive r) (h : ∀ (a ∈ l) (b ∈ l), a ≠ b → r a b) : l.pairwise r :=
+by { classical, exact pairwise_of_reflexive_on_dupl_of_forall_ne (λ _ _, hr _) h }
+
 theorem pairwise_iff_nth_le {R} : ∀ {l : list α},
   pairwise R l ↔ ∀ i j (h₁ : j < length l) (h₂ : i < j),
     R (nth_le l i (lt_trans h₂ h₁)) (nth_le l j h₁)