chore: upstream List.Pairwise lemmas (#5047)

src/Init/Data/List/Lemmas.lean

@@ -256,6 +256,10 @@ theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length
 
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
+theorem getElem?_eq (l : List α) (i : Nat) :
+    l[i]? = if h : i < l.length then some l[i] else none := by
+  split <;> simp_all
+
 theorem getElem_eq_iff {l : List α} {n : Nat} {h : n < l.length} : l[n] = x ↔ l[n]? = some x := by
   simp only [getElem?_eq_some]
   exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩

src/Init/Data/List/Pairwise.lean

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Sublist
+import Init.Data.List.Attach
 
 /-!
 # Lemmas about `List.Pairwise` and `List.Nodup`.
@@ -225,6 +226,31 @@ theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l
         intro a b hab
         apply h; exact hab.cons _
 
+theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h : ∀ a ∈ l, ∀ b ∈ l, r a b) :
+    l.Pairwise r := by
+  rw [pairwise_iff_forall_sublist]
+  intro a b hab
+  apply h <;> (apply hab.subset; simp)
+
+theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
+    Pairwise R (l.pmap f h) ↔
+      Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l := by
+  induction l with
+  | nil => simp
+  | cons a l ihl =>
+    obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
+    simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]
+    refine fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, ?_⟩
+    rintro H _ b hb rfl
+    exact H b hb _ _
+
+theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
+    (h : ∀ x ∈ l, p x) {S : β → β → Prop}
+    (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
+    Pairwise S (l.pmap f h) := by
+  refine (pairwise_pmap h).2 (Pairwise.imp_of_mem ?_ hl)
+  intros; apply hS; assumption
+
 /-! ### Nodup -/
 
 @[simp]

src/Init/PropLemmas.lean

@@ -198,6 +198,7 @@ theorem Exists.imp' {β} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a →
   | ⟨_, hp⟩ => ⟨_, hpq _ hp⟩
 
 theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_index
+theorem exists₂_imp {P : (x : α) → p x → Prop} : (∃ x h, P x h) → b ↔ ∀ x h, P x h → b := by simp
 
 @[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
   ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩