Group consecutive elements in a list by a relation

This file provides the basic API for List.groupBy which is defined in Core. The main results are the following:

• List.join_groupBy: the lists in List.groupBy join to the original list.
• List.nil_not_mem_groupBy: the empty list is not contained in List.groupBy.
• List.chain'_of_mem_groupBy: any two adjacent elements in a list in List.groupBy are related by the specified relation.
• List.chain'_getLast_head_groupBy: the last element of each list in List.groupBy is not related to the first element of the next list.

@[simp]

theorem List.groupBy_nil {α : Type u_1} (r : α → α → Bool) : List.groupBy r [] = []

@[simp]

theorem List.join_groupBy {α : Type u_1} (r : α → α → Bool) (l : List α) : (List.groupBy r l).join = l

theorem List.nil_not_mem_groupBy {α : Type u_1} (r : α → α → Bool) (l : List α) : ¬[] ∈ List.groupBy r l

theorem List.ne_nil_of_mem_groupBy {α : Type u_1} {m : List α} (r : α → α → Bool) {l : List α} (h : m ∈ List.groupBy r l) : m ≠ []

theorem List.chain'_of_mem_groupBy {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} (h : m ∈ List.groupBy r l) : List.Chain' (fun (x y : α) => r x y = true) m

theorem List.chain'_getLast_head_groupBy {α : Type u_1} (r : α → α → Bool) (l : List α) : List.Chain' (fun (a b : List α) => ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (List.groupBy r l)