.

src/Init/Data/List/Find.lean

@@ -236,10 +236,54 @@ theorem find?_join_eq_none (xs : List (List α)) (p : α → Bool) :
     xs.join.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
+/--
+If `find? p` returns `some a` from `xs.join`, then `p a` holds, and
+some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
+Moreover, no earlier list in `xs` has an element satisfying `p`.
+-/
+theorem find?_join_eq_some (xs : List (List α)) (p : α → Bool) (a : α) :
+    xs.join.find? p = some a ↔
+      p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
+        (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
+  rw [find?_eq_some]
+  constructor
+  · rintro ⟨h, ⟨ys, zs, h₁, h₂⟩⟩
+    refine ⟨h, ?_⟩
+    rw [join_eq_append] at h₁
+    obtain (⟨as, bs, rfl, rfl, h₁⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h₁⟩) := h₁
+    · replace h₁ := h₁.symm
+      rw [join_eq_cons] at h₁
+      obtain ⟨bs, cs, ds, rfl, h₁, rfl⟩ := h₁
+      refine ⟨as ++ bs, [], cs, ds, by simp, ?_⟩
+      simp
+      rintro a (ma | mb) x m
+      · simpa using h₂ x (by simpa using ⟨a, ma, m⟩)
+      · specialize h₁ _ mb
+        simp_all
+    · simp [h₁]
+      refine ⟨as, bs, ?_⟩
+      refine ⟨?_, ?_, ?_⟩
+      · simp_all
+      · intro l ml a m
+        simpa using h₂ a (by simpa using .inl ⟨l, ml, m⟩)
+      · intro x m
+        simpa using h₂ x (by simpa using .inr m)
+  · rintro ⟨h, ⟨as, ys, zs, bs, rfl, h₁, h₂⟩⟩
+    refine ⟨h, as.join ++ ys, zs ++ bs.join, by simp, ?_⟩
+    intro a m
+    simp at m
+    obtain ⟨l, ml, m⟩ | m := m
+    · exact h₁ l ml a m
+    · exact h₂ a m
+
 @[simp] theorem find?_bind (xs : List α) (f : α → List β) (p : β → Bool) :
     (xs.bind f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [bind_def]; rfl
 
+theorem find?_bind_eq_none (xs : List α) (f : α → List β) (p : β → Bool) :
+    (xs.bind f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+  simp
+
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp

src/Init/Data/List/Lemmas.lean

@@ -79,6 +79,11 @@ open Nat
 
 /-! ## Preliminaries -/
 
+/-! ### nil -/
+
+@[simp] theorem nil_eq {α} (xs : List α) : [] = xs ↔ xs = [] := by
+  cases xs <;> simp
+
 /-! ### cons -/
 
 theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun
@@ -1771,6 +1776,55 @@ theorem join_concat (L : List (List α)) (l : List α) : join (L ++ [l]) = join
 theorem join_join {L : List (List (List α))} : join (join L) = join (map join L) := by
   induction L <;> simp_all
 
+theorem join_eq_cons (xs : List (List α)) (y : α) (ys : List α) :
+    xs.join = y :: ys ↔
+      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.join := by
+  constructor
+  · induction xs with
+    | nil => simp
+    | cons x xs ih =>
+      intro h
+      simp only [join_cons] at h
+      replace h := h.symm
+      rw [cons_eq_append] at h
+      obtain (⟨rfl, h⟩ | ⟨z⟩) := h
+      · obtain ⟨as, bs, cs, rfl, _, rfl⟩ := ih h
+        refine ⟨[] :: as, bs, cs, ?_⟩
+        simpa
+      · obtain ⟨a', rfl, rfl⟩ := z
+        refine ⟨[], a', xs, ?_⟩
+        simp
+  · rintro ⟨as, bs, cs, rfl, h₁, rfl⟩
+    simp [join_eq_nil.mpr h₁]
+
+theorem join_eq_append (xs : List (List α)) (ys zs : List α) :
+    xs.join = ys ++ zs ↔
+      (∃ as bs, xs = as ++ bs ∧ ys = as.join ∧ zs = bs.join) ∨
+        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.join ++ bs ∧
+          zs = c :: cs ++ ds.join := by
+  constructor
+  · induction xs generalizing ys with
+    | nil =>
+      simp only [join_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
+        exists_false, or_false, and_imp]
+      rintro rfl rfl
+      exact ⟨[], [], by simp⟩
+    | cons x xs ih =>
+      intro h
+      simp only [join_cons] at h
+      rw [append_eq_append_iff] at h
+      obtain (⟨ys, rfl, h⟩ | ⟨c', rfl, h⟩) := h
+      · obtain (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩) := ih _ h
+        · exact .inl ⟨x :: as, bs, by simp⟩
+        · exact .inr ⟨x :: as, bs, c, cs, ds, by simp⟩
+      · simp only [h]
+        cases c' with
+        | nil => exact .inl ⟨[ys], xs, by simp⟩
+        | cons x c' => exact .inr ⟨[], ys, x, c', xs, by simp⟩
+  · rintro (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩)
+    · simp
+    · simp
+
 /-- Two lists of sublists are equal iff their joins coincide, as well as the lengths of the
 sublists. -/
 theorem eq_iff_join_eq : ∀ (L L' : List (List α)),