Merge remote-tracking branch 'origin/master' into find_theorems

src/Init/Data/List/Erase.lean

@@ -159,6 +159,15 @@ theorem eraseP_append (l₁ l₂ : List α) :
     rw [eraseP_append_right _]
     simp_all
 
+protected theorem IsPrefix.eraseP (h : l₁ <+: l₂) : l₁.eraseP p <+: l₂.eraseP p := by
+  rw [IsPrefix] at h
+  obtain ⟨t, rfl⟩ := h
+  rw [eraseP_append]
+  split
+  · exact prefix_append (eraseP p l₁) t
+  · rw [eraseP_of_forall_not (by simp_all)]
+    exact prefix_append l₁ (eraseP p t)
+
 theorem eraseP_eq_iff {p} {l : List α} :
     l.eraseP p = l' ↔
       ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
@@ -271,6 +280,9 @@ theorem erase_subset (a : α) (l : List α) : l.erase a ⊆ l := (erase_sublist
 theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by
   simp only [erase_eq_eraseP']; exact h.eraseP
 
+theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.erase a <+: l₂.erase a := by
+  simp only [erase_eq_eraseP']; exact h.eraseP
+
 theorem length_erase_le (a : α) (l : List α) : (l.erase a).length ≤ l.length :=
   (erase_sublist a l).length_le
 

src/Init/Data/List/Find.lean

@@ -6,6 +6,8 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Lemmas
+import Init.Data.List.Sublist
+import Init.Data.List.Range
 
 /-!
 # Lemmas about `List.find?`, `List.findSome?`, `List.findIdx`, `List.findIdx?`, and `List.indexOf`.
@@ -45,6 +47,13 @@ theorem find?_some : ∀ {l}, find? p l = some a → p a
     simp only [map_cons, find?]
     by_cases h : p (f x) <;> simp [h, ih]
 
+theorem find?_append {l₁ l₂ : List α} : (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [cons_append, find?]
+    by_cases h : p x <;> simp [h, ih]
+
 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
@@ -59,7 +68,7 @@ theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
-theorem find?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.find? p).isSome → (l₂.find? p).isSome := by
+theorem Sublist.find?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.find? p).isSome → (l₂.find? p).isSome := by
   induction h with
   | slnil => simp
   | cons a h ih
@@ -67,6 +76,26 @@ theorem find?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁
     simp only [find?]
     split <;> simp_all
 
+theorem Sublist.find?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₂.find? p = none → l₁.find? p = none := by
+  simp only [List.find?_eq_none, Bool.not_eq_true]
+  exact fun w x m => w x (Sublist.mem m h)
+
+theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
+    List.find? p l₁ = some b → List.find? p l₂ = some b := by
+  rw [IsPrefix] at h
+  obtain ⟨t, rfl⟩ := h
+  simp (config := {contextual := true}) [find?_append]
+
+theorem IsPrefix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
+    List.find? p l₂ = none → List.find? p l₁ = none :=
+  h.sublist.find?_eq_none
+theorem IsSuffix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) :
+    List.find? p l₂ = none → List.find? p l₁ = none :=
+  h.sublist.find?_eq_none
+theorem IsInfix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) :
+    List.find? p l₂ = none → List.find? p l₁ = none :=
+  h.sublist.find?_eq_none
+
 /-! ### findSome? -/
 
 @[simp] theorem findSome?_cons_of_isSome (l) (h : (f a).isSome) : findSome? f (a :: l) = f a := by
@@ -85,6 +114,13 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
     split at w <;> simp_all
 
+@[simp] theorem findSome?_eq_none : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+  induction l <;> simp [findSome?_cons]; split <;> simp [*]
+
+@[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : List α) :
+    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
+  induction l <;> simp [findSome?_cons]; split <;> simp [*]
+
 @[simp] theorem findSome?_map (f : β → γ) (l : List β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
   induction l with
   | nil => simp
@@ -92,10 +128,17 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp only [map_cons, findSome?]
     split <;> simp_all
 
+theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [cons_append, findSome?]
+    split <;> simp_all
+
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
-  induction n with
+  cases n with
   | zero => simp
-  | succ n ih =>
+  | succ n =>
     simp only [replicate_succ, findSome?_cons]
     split <;> simp_all
 
@@ -110,7 +153,7 @@ theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none e
   rw [Option.isNone_iff_eq_none] at h
   simp [findSome?_replicate, h]
 
-theorem findSome?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     (l₁.findSome? f).isSome → (l₂.findSome? f).isSome := by
   induction h with
   | slnil => simp
@@ -119,6 +162,27 @@ theorem findSome?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     simp only [findSome?]
     split <;> simp_all
 
+theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+    l₂.findSome? f = none → l₁.findSome? f = none := by
+  simp only [List.findSome?_eq_none, Bool.not_eq_true]
+  exact fun w x m => w x (Sublist.mem m h)
+
+theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
+    List.findSome? f l₁ = some b → List.findSome? f l₂ = some b := by
+  rw [IsPrefix] at h
+  obtain ⟨t, rfl⟩ := h
+  simp (config := {contextual := true}) [findSome?_append]
+
+theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
+    List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
+  h.sublist.findSome?_eq_none
+theorem IsSuffix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+ l₂) :
+    List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
+  h.sublist.findSome?_eq_none
+theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+: l₂) :
+    List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
+  h.sublist.findSome?_eq_none
+
 /-! ### findIdx -/
 
 theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
@@ -163,8 +227,7 @@ theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
     · simp_all only [forall_exists_index, and_imp, mem_cons, exists_eq_or_imp, true_or,
         findIdx_cons, cond_true, length_cons]
       apply Nat.succ_pos
-    · simp_all [findIdx_cons]
-      refine Nat.succ_lt_succ ?_
+    · simp_all [findIdx_cons, Nat.succ_lt_succ_iff]
       obtain ⟨x', m', h'⟩ := h
       exact ih x' m' h'
 
@@ -187,6 +250,11 @@ theorem findIdx_eq_length {p : α → Bool} {xs : List α} :
     simp only [cond_eq_if]
     split <;> simp_all [Nat.succ.injEq]
 
+theorem findIdx_eq_length_of_false {p : α → Bool} {xs : List α} (h : ∀ x ∈ xs, p x = false) :
+    xs.findIdx p = xs.length := by
+  rw [findIdx_eq_length]
+  exact h
+
 theorem findIdx_le_length (p : α → Bool) {xs : List α} : xs.findIdx p ≤ xs.length := by
   by_cases e : ∃ x ∈ xs, p x
   · exact Nat.le_of_lt (findIdx_lt_length_of_exists e)
@@ -250,6 +318,38 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
   simp at h3
   exact not_of_lt_findIdx h3 h1
 
+theorem findIdx_append (p : α → Bool) (l₁ l₂ : List α) :
+    (l₁ ++ l₂).findIdx p =
+      if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length := by
+  simp
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx_cons, length_cons, cons_append]
+    by_cases h : p x
+    · simp [h]
+    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, mem_cons, exists_eq_or_imp,
+        false_or]
+      split <;> simp [Nat.add_assoc]
+
+theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
+    l₁.findIdx p ≤ l₂.findIdx p := by
+  rw [IsPrefix] at h
+  obtain ⟨t, rfl⟩ := h
+  simp only [findIdx_append, findIdx_lt_length]
+  split
+  · exact Nat.le_refl ..
+  · simp_all [findIdx_eq_length_of_false]
+
+theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂)
+    (lt : l₁.findIdx p < l₁.length) : l₂.findIdx p = l₁.findIdx p := by
+  rw [IsPrefix] at h
+  obtain ⟨t, rfl⟩ := h
+  simp only [findIdx_append, findIdx_lt_length]
+  split
+  · rfl
+  · simp_all
+
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
@@ -262,16 +362,91 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
   induction xs generalizing i with simp
   | cons _ _ _ => split <;> simp_all
 
-theorem findIdx?_eq_some_iff (xs : List α) (p : α → Bool) :
-    xs.findIdx? p = some i ↔ (xs.take (i + 1)).map p = replicate i false ++ [true] := by
+@[simp]
+theorem findIdx?_eq_none_iff {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false := by
+  induction xs with
+  | nil => simp_all
+  | cons x xs ih =>
+    simp only [findIdx?_cons]
+    split <;> simp_all [cond_eq_if]
+
+theorem findIdx?_isSome {xs : List α} {p : α → Bool} :
+    (xs.findIdx? p).isSome = xs.any p := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx?_cons]
+    split <;> simp_all
+
+theorem findIdx?_isNone {xs : List α} {p : α → Bool} :
+    (xs.findIdx? p).isNone = xs.all (¬p ·) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx?_cons]
+    split <;> simp_all
+
+theorem findIdx?_eq_some_iff_findIdx_eq {xs : List α} {p : α → Bool} {i : Nat} :
+    xs.findIdx? p = some i ↔ i < xs.length ∧ xs.findIdx p = i := by
+  induction xs generalizing i with
+  | nil => simp_all
+  | cons x xs ih =>
+    simp only [findIdx?_cons, findIdx_cons]
+    split
+    · simp_all [cond_eq_if]
+      rintro rfl
+      exact zero_lt_succ xs.length
+    · simp_all [cond_eq_if, and_assoc]
+      constructor
+      · rintro ⟨a, lt, rfl, rfl⟩
+        simp_all [Nat.succ_lt_succ_iff]
+      · rintro ⟨h, rfl⟩
+        exact ⟨_, by simp_all [Nat.succ_lt_succ_iff], rfl, rfl⟩
+
+theorem findIdx?_eq_some_of_exists {xs : List α} {p : α → Bool} (h : ∃ x, x ∈ xs ∧ p x) :
+    xs.findIdx? p = some (xs.findIdx p) := by
+  rw [findIdx?_eq_some_iff_findIdx_eq]
+  exact ⟨findIdx_lt_length_of_exists h, rfl⟩
+
+theorem findIdx?_eq_none_iff_findIdx_eq {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = none ↔ xs.findIdx p = xs.length := by
+  simp
+
+theorem findIdx?_eq_some_iff_getElem (xs : List α) (p : α → Bool) :
+    xs.findIdx? p = some i ↔
+      ∃ h : i < xs.length, p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h)) := by
   induction xs generalizing i with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, take_succ_cons, map_cons]
-    split <;> cases i <;> simp_all [replicate_succ, succ_inj']
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ]
+    split
+    · simp only [Option.some.injEq, Bool.not_eq_true, length_cons]
+      cases i with
+      | zero => simp_all
+      | succ i =>
+        simp only [Bool.not_eq_true, zero_ne_add_one, getElem_cons_succ, false_iff, not_exists,
+          not_and, Classical.not_forall, Bool.not_eq_false]
+        intros
+        refine ⟨0, zero_lt_succ i, ‹_›⟩
+    · simp only [Option.map_eq_some', ih, Bool.not_eq_true, length_cons]
+      constructor
+      · rintro ⟨a, ⟨⟨h, h₁, h₂⟩, rfl⟩⟩
+        refine ⟨Nat.succ_lt_succ_iff.mpr h, by simpa, fun j hj => ?_⟩
+        cases j with
+        | zero => simp_all
+        | succ j =>
+          apply h₂
+          simp_all [Nat.succ_lt_succ_iff]
+      · rintro ⟨h, h₁, h₂⟩
+        cases i with
+        | zero => simp_all
+        | succ i =>
+          refine ⟨i, ⟨Nat.succ_lt_succ_iff.mp h, by simpa, fun j hj => ?_⟩, rfl⟩
+          simpa using h₂ (j + 1) (Nat.succ_lt_succ_iff.mpr hj)
 
 theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) :
-    match xs.get? i with | some a => p a | none => false := by
+    match xs[i]? with | some a => p a | none => false := by
   induction xs generalizing i with
   | nil => simp_all
   | cons x xs ih =>
@@ -279,7 +454,7 @@ theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
     split at w <;> cases i <;> simp_all [succ_inj']
 
 theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
-    ∀ i, match xs.get? i with | some a => ¬ p a | none => true := by
+    ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true := by
   intro i
   induction xs generalizing i with
   | nil => simp_all
@@ -289,24 +464,90 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
     | zero =>
       split at w <;> simp_all
     | succ i =>
-      simp only [get?_cons_succ]
+      simp only [getElem?_cons_succ]
       apply ih
       split at w <;> simp_all
 
+@[simp] theorem findIdx?_map (f : β → α) (l : List β) : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [map_cons, findIdx?]
+    split <;> simp_all
+
 @[simp] theorem findIdx?_append :
     (xs ++ ys : List α).findIdx? p =
-      (xs.findIdx? p <|> (ys.findIdx? p).map fun i => i + xs.length) := by
+      (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.length) := by
   induction xs with simp
-  | cons _ _ _ => split <;> simp_all [Option.map_orElse, Option.map_map]; rfl
+  | cons _ _ _ => split <;> simp_all [Option.map_or', Option.map_map]; rfl
+
+theorem findIdx?_join {l : List (List α)} {p : α → Bool} :
+    l.join.findIdx? p =
+      (l.findIdx? (·.any p)).map
+        fun i => Nat.sum ((l.take i).map List.length) +
+          (l[i]?.map fun xs => xs.findIdx p).getD 0 := by
+  induction l with
+  | nil => simp
+  | cons xs l ih =>
+    simp only [join, findIdx?_append, map_take, map_cons, findIdx?, any_eq_true, Nat.zero_add,
+      findIdx?_succ]
+    split
+    · simp only [Option.map_some', take_zero, sum_nil, length_cons, zero_lt_succ,
+        getElem?_eq_getElem, getElem_cons_zero, Option.getD_some, Nat.zero_add]
+      rw [Option.or_of_isSome (by simpa [findIdx?_isSome])]
+      rw [findIdx?_eq_some_of_exists ‹_›]
+    · simp_all only [map_take, not_exists, not_and, Bool.not_eq_true, Option.map_map]
+      rw [Option.or_of_isNone (by simpa [findIdx?_isNone])]
+      congr 1
+      ext i
+      simp [Nat.add_comm, Nat.add_assoc]
 
 @[simp] theorem findIdx?_replicate :
     (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
-  induction n with
+  cases n with
   | zero => simp
-  | succ n ih =>
-    simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, Nat.zero_lt_succ, true_and]
+  | succ n =>
+    simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
     split <;> simp_all
 
+theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = xs.enum.findSome? fun ⟨i, a⟩ => if p a then some i else none := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
+    split
+    · simp_all
+    · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
+      simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom]
+
+theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+    (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome := by
+  simp only [List.findIdx?_isSome, any_eq_true]
+  rintro ⟨w, m, q⟩
+  exact ⟨w, h.mem m, q⟩
+
+theorem Sublist.findIdx?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+    l₂.findIdx? p = none → l₁.findIdx? p = none := by
+  simp only [findIdx?_eq_none_iff]
+  exact fun w x m => w x (h.mem m)
+
+theorem IsPrefix.findIdx?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
+    List.findIdx? p l₁ = some i → List.findIdx? p l₂ = some i := by
+  rw [IsPrefix] at h
+  obtain ⟨t, rfl⟩ := h
+  intro h
+  simp [findIdx?_append, h]
+theorem IsPrefix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
+    List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
+  h.sublist.findIdx?_eq_none
+theorem IsSuffix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) :
+    List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
+  h.sublist.findIdx?_eq_none
+theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) :
+    List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
+  h.sublist.findIdx?_eq_none
+
 /-! ### indexOf -/
 
 theorem indexOf_cons [BEq α] :

src/Init/Data/List/Nat/Range.lean

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Range
 import Init.Data.List.Pairwise
 
 /-!
@@ -219,31 +220,6 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
 theorem enumFrom_singleton (x : α) (n : Nat) : enumFrom n [x] = [(n, x)] :=
   rfl
 
-@[simp]
-theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = [] := by
-  cases l <;> simp
-
-@[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
-  | _, [] => rfl
-  | _, _ :: _ => congrArg Nat.succ enumFrom_length
-
-@[simp]
-theorem getElem?_enumFrom :
-    ∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a)
-  | n, [], m => rfl
-  | n, a :: l, 0 => by simp
-  | n, a :: l, m + 1 => by
-    simp only [enumFrom_cons, getElem?_cons_succ]
-    exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl
-
-@[simp]
-theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) :
-    (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h)) := by
-  simp only [enumFrom_length] at h
-  rw [getElem_eq_getElem?]
-  simp only [getElem?_enumFrom, getElem?_eq_getElem h]
-  simp
-
 theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} :
     (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x := by
   simp [mem_iff_get?]
@@ -288,14 +264,6 @@ theorem mem_enumFrom {x : α} {i j : Nat} (xs : List α) (h : (i, x) ∈ xs.enum
     j ≤ i ∧ i < j + xs.length ∧ x ∈ xs :=
   ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_mem_of_mem_enumFrom h⟩
 
-theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
-    map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
-  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
-
-theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
-    map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
-  map_fst_add_enumFrom_eq_enumFrom l _ _
-
 theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
     enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
   rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]

src/Init/Data/List/Range.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Pairwise
+
+/-!
+# Lemmas about `List.range` and `List.enum`
+
+Most of the results are deferred to `Data.Init.List.Nat.Range`, where more results about
+natural arithmetic are available.
+-/
+
+namespace List
+
+open Nat
+
+/-! ## Ranges and enumeration -/
+
+/-! ### enumFrom -/
+
+@[simp]
+theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = [] := by
+  cases l <;> simp
+
+@[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
+  | _, [] => rfl
+  | _, _ :: _ => congrArg Nat.succ enumFrom_length
+
+@[simp]
+theorem getElem?_enumFrom :
+    ∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a)
+  | n, [], m => rfl
+  | n, a :: l, 0 => by simp
+  | n, a :: l, m + 1 => by
+    simp only [enumFrom_cons, getElem?_cons_succ]
+    exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl
+
+@[simp]
+theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) :
+    (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h)) := by
+  simp only [enumFrom_length] at h
+  rw [getElem_eq_getElem?]
+  simp only [getElem?_enumFrom, getElem?_eq_getElem h]
+  simp
+
+theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
+    map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
+  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
+
+theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
+    map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
+  map_fst_add_enumFrom_eq_enumFrom l _ _
+
+end List

src/Init/Data/List/Sublist.lean

@@ -180,6 +180,9 @@ theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
   | .cons₂ .., _, .head .. => .head ..
   | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h)
 
+protected theorem Sublist.mem (hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂ :=
+  hl.subset hx
+
 instance : Trans (@Sublist α) Subset Subset :=
   ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
 

src/Init/Data/Option/Lemmas.lean

@@ -167,6 +167,9 @@ theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
 @[simp] theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome := by
   cases x <;> simp
 
+@[simp] theorem isNone_map' {x : Option α} : (x.map f).isNone = x.isNone := by
+  cases x <;> simp
+
 theorem map_eq_none : f <$> x = none ↔ x = none := map_eq_none'
 
 theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f) := by
@@ -190,6 +193,14 @@ theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘
 
 theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some' ..
 
+@[simp] theorem map_if {f : α → β} [Decidable c] :
+     (if c then some a else none).map f = if c then some (f a) else none := by
+  split <;> rfl
+
+@[simp] theorem map_dif {f : α → β} [Decidable c] {a : c → α} :
+     (if h : c then some (a h) else none).map f = if h : c then some (f (a h)) else none := by
+  split <;> rfl
+
 @[simp] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
 theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
 
@@ -314,3 +325,11 @@ theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by
 
 theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by
   cases o <;> rfl
+
+theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o := by
+  match o, h with
+  | some _, _ => simp
+
+theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o' := by
+  match o, h with
+  | none, _ => simp