From 76ea33c4c6c382b7feefd1736e459bb97862d9fe Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Thu, 5 Sep 2024 23:08:31 +1000
Subject: [PATCH 01/11] chore: review of List API (#5264)

---
 src/Init/Data/List/Find.lean     | 142 ++++++++++++++++++++++++++++++-
 src/Init/Data/List/Lemmas.lean   | 108 ++++++++++++-----------
 src/Init/Data/List/TakeDrop.lean |  12 +++
 3 files changed, 205 insertions(+), 57 deletions(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index cde4aab1c504..771a3dd41bb2 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -35,9 +35,11 @@ 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
+@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
+@[deprecated findSome?_eq_none_iff (since := "2024-09-05")] abbrev findSome?_eq_none := @findSome?_eq_none_iff
+
 @[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
     (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
   induction l with
@@ -46,6 +48,41 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp only [findSome?_cons]
     split <;> simp_all
 
+theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
+    l.findSome? f = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
+  induction l with
+  | nil => simp
+  | cons p l ih =>
+    simp only [findSome?_cons]
+    split <;> rename_i b' h
+    · simp only [Option.some.injEq, exists_and_right]
+      constructor
+      · rintro rfl
+        exact ⟨[], p, ⟨l, rfl⟩, h, by simp⟩
+      · rintro ⟨(⟨⟩ | ⟨p', l₁⟩), a, ⟨l₂, h₁⟩, h₂, h₃⟩
+        · simp only [nil_append, cons.injEq] at h₁
+          apply Option.some.inj
+          simp [← h, ← h₂, h₁.1]
+        · simp only [cons_append, cons.injEq] at h₁
+          obtain ⟨rfl, rfl⟩ := h₁
+          specialize h₃ p
+          simp_all
+    · rw [ih]
+      constructor
+      · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+        refine ⟨p :: l₁, a, l₂, rfl, h₁, ?_⟩
+        intro a w
+        simp at w
+        rcases w with rfl | w
+        · exact h
+        · exact h₂ _ w
+      · rintro ⟨l₁, a, l₂, h₁, h₂, h₃⟩
+        rcases l₁ with (⟨⟩ | ⟨a', l₁⟩)
+        · simp_all
+        · simp only [cons_append, cons.injEq] at h₁
+          obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h₁
+          exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩
+
 @[simp] theorem findSome?_guard (l : List α) : findSome? (Option.guard fun x => p x) l = find? p l := by
   induction l with
   | nil => simp
@@ -95,6 +132,15 @@ theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l
     simp only [cons_append, findSome?]
     split <;> simp_all
 
+theorem head_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
+    (join L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
+  simp [head_eq_iff_head?_eq_some, head?_join]
+
+theorem getLast_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
+    (join L).getLast (by simpa using h) =
+      (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
+  simp [getLast_eq_iff_getLast_eq_some, getLast?_join]
+
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   cases n with
   | zero => simp
@@ -126,7 +172,7 @@ theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
 
 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]
+  simp only [List.findSome?_eq_none_iff, 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₂) :
@@ -776,4 +822,96 @@ theorem indexOf_cons [BEq α] :
   dsimp [indexOf]
   simp [findIdx_cons]
 
+/-! ### lookup -/
+section lookup
+variable [BEq α] [LawfulBEq α]
+
+@[simp] theorem lookup_cons_self  {k : α} : ((k,b) :: es).lookup k = some b := by
+  simp [lookup_cons]
+
+theorem lookup_eq_findSome? (l : List (α × β)) (k : α) :
+    l.lookup k = l.findSome? fun p => if k == p.1 then some p.2 else none := by
+  induction l with
+  | nil => rfl
+  | cons p l ih =>
+    match p with
+    | (k', v) =>
+      simp only [lookup_cons, findSome?_cons]
+      split <;> simp_all
+
+@[simp] theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
+    l.lookup k = none ↔ ∀ p ∈ l, k != p.1 := by
+  simp [lookup_eq_findSome?]
+
+@[simp] theorem lookup_isSome_iff {l : List (α × β)} {k : α} :
+    (l.lookup k).isSome ↔ ∃ p ∈ l, k == p.1 := by
+  simp [lookup_eq_findSome?]
+
+theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
+    l.lookup k = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ p ∈ l₁, k != p.1 := by
+  simp only [lookup_eq_findSome?, findSome?_eq_some_iff]
+  constructor
+  · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+    simp only [beq_iff_eq, ite_some_none_eq_some] at h₁
+    obtain ⟨rfl, rfl⟩ := h₁
+    simp at h₂
+    exact ⟨l₁, l₂, rfl, by simpa using h₂⟩
+  · rintro ⟨l₁, l₂, rfl, h⟩
+    exact ⟨l₁, (k, b), l₂, rfl, by simp, by simpa using h⟩
+
+theorem lookup_append {l₁ l₂ : List (α × β)} {k : α} :
+    (l₁ ++ l₂).lookup k = (l₁.lookup k).or (l₂.lookup k) := by
+  simp [lookup_eq_findSome?, findSome?_append]
+
+theorem lookup_replicate {k : α} :
+    (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, lookup_cons]
+    split <;> simp_all
+
+theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
+    (replicate n (a, b)).lookup k = if k == a then some b else none := by
+  simp [lookup_replicate, Nat.ne_of_gt h]
+
+theorem lookup_replicate_self {a : α} :
+    (replicate n (a, b)).lookup a = if n = 0 then none else some b := by
+  simp [lookup_replicate]
+
+@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
+    (replicate n (a, b)).lookup a = some b := by
+  simp [lookup_replicate_self, Nat.ne_of_gt h]
+
+@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
+    (replicate n (a, b)).lookup k = none := by
+  simp_all [lookup_replicate]
+
+theorem Sublist.lookup_isSome {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
+    (l₁.lookup k).isSome → (l₂.lookup k).isSome := by
+  simp only [lookup_eq_findSome?]
+  exact h.findSome?_isSome
+
+theorem Sublist.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
+    l₂.lookup k = none → l₁.lookup k = none := by
+  simp only [lookup_eq_findSome?]
+  exact h.findSome?_eq_none
+
+theorem IsPrefix.lookup_eq_some {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
+    List.lookup k l₁ = some b → List.lookup k l₂ = some b := by
+  simp only [lookup_eq_findSome?]
+  exact h.findSome?_eq_some
+
+theorem IsPrefix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
+    List.lookup k l₂ = none → List.lookup k l₁ = none :=
+  h.sublist.lookup_eq_none
+theorem IsSuffix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+ l₂) :
+    List.lookup k l₂ = none → List.lookup k l₁ = none :=
+  h.sublist.lookup_eq_none
+theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) :
+    List.lookup k l₂ = none → List.lookup k l₁ = none :=
+  h.sublist.lookup_eq_none
+
+end lookup
+
 end List
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index d771da16f689..6500c77c6416 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -939,8 +939,8 @@ theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
   rw [getLast?_eq_getLast _ h]
   simp
 
--- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, and `getLast_mem` are proved later
--- once more `reverse` theorems are available.
+-- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, `getLast?_isSome`, and `getLast_mem`
+-- are proved later once more `reverse` theorems are available.
 
 theorem getLast?_cons {a : α} : (a::l).getLast? = l.getLast?.getD a := by
   cases l <;> simp [getLast?, getLast]
@@ -986,6 +986,9 @@ theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head
 theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys, xs = a :: ys := by
   cases xs <;> simp_all
 
+@[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
+  cases l <;> simp
+
 @[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
   | [], h => absurd rfl h
   | _::_, _ => .head ..
@@ -1151,6 +1154,10 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
 @[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
   cases l <;> rfl
 
+@[simp] theorem tail_map (f : α → β) (l : List α) :
+    (map f l).tail = map f l.tail := by
+  cases l <;> simp_all
+
 theorem headD_map (f : α → β) (l : List α) (a : α) : headD (map f l) (f a) = f (headD l a) := by
   cases l <;> rfl
 
@@ -1643,9 +1650,27 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
 -- are stated and proved later in the `reverse` section.
 
-theorem nil_eq_append : [] = a ++ b ↔ a = [] ∧ b = [] := by
+theorem tail?_append {l l' : List α} : (l ++ l').tail? = (l.tail?.map (· ++ l')).or l'.tail? := by
+  cases l <;> simp
+
+theorem tail?_append_of_ne_nil {l l' : List α} (_ : l ≠ []) : (l ++ l').tail? = some (l.tail ++ l') :=
+  match l with
+  | _ :: _ => by simp
+
+theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tail else l.tail ++ l' := by
+  cases l <;> simp
+
+@[simp] theorem tail_append_of_ne_nil {xs ys : List α} (h : xs ≠ []) :
+    (xs ++ ys).tail = xs.tail ++ ys := by
+  simp_all [tail_append]
+
+@[deprecated tail_append_of_ne_nil (since := "2024-07-24")] abbrev tail_append_left := @tail_append_of_ne_nil
+
+theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
   rw [eq_comm, append_eq_nil]
 
+@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
+
 theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
 theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
@@ -1654,22 +1679,6 @@ theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α)
 @[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
 theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
-theorem tail_append (xs ys : List α) :
-    (xs ++ ys).tail = if xs.isEmpty then ys.tail else xs.tail ++ ys := by
-  cases xs <;> simp
-
-theorem tail_append_left {xs ys : List α} (h : xs ≠ []) :
-    (xs ++ ys).tail = xs.tail ++ ys := by
-  simp [tail_append, h]
-
-theorem tail_append_right {xs ys : List α} (h : ys = []) :
-    (xs ++ ys).tail = xs.tail := by
-  simp [tail_append, h]
-
-@[simp] theorem tail_append_of_ne_nil (xs ys : List α) (h : xs ≠ []) :
-    (xs ++ ys).tail = xs.tail ++ ys := by
-  simp_all [tail_append]
-
 theorem append_eq_cons_iff :
     a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
   cases a with simp | cons a as => ?_
@@ -1749,7 +1758,7 @@ theorem filterMap_eq_append_iff {f : α → Option β} :
   constructor
   · induction l generalizing L₁ with
     | nil =>
-      simp only [filterMap_nil, nil_eq_append, and_imp]
+      simp only [filterMap_nil, nil_eq_append_iff, and_imp]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
     | cons x l ih =>
@@ -1895,7 +1904,8 @@ theorem head?_join {L : List (List α)} : (join L).head? = L.findSome? fun l =>
     simp only [findSome?_cons]
     split <;> simp_all
 
--- `getLast?_join` is proved later, after the `reverse` section
+-- `getLast?_join` is proved later, after the `reverse` section.
+-- `head_join` and `getLast_join` are proved in `Init.Data.List.Find`.
 
 theorem foldl_join (f : β → α → β) (b : β) (L : List (List α)) :
     (join L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@@ -2465,6 +2475,10 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
   simp only [reverse_eq_cons_iff]
   exact ⟨fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩, fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩⟩
 
+@[simp] theorem getLast?_isSome : l.getLast?.isSome ↔ l ≠ [] := by
+  rw [getLast?_eq_head?_reverse, head?_isSome]
+  simp
+
 theorem mem_of_getLast?_eq_some {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
   obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.1 h
   exact mem_concat_self ys a
@@ -2790,6 +2804,14 @@ theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
     simp only [cons_append, replace_cons]
     split <;> split <;> simp_all
 
+theorem replace_append_left [LawfulBEq α] {l₁ l₂ : List α} (h : a ∈ l₁) :
+    (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂ := by
+  simp [replace_append, h]
+
+theorem replace_append_right [LawfulBEq α] {l₁ l₂ : List α} (h : ¬ a ∈ l₁) :
+    (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b := by
+  simp [replace_append, h]
+
 theorem replace_take {l : List α} {n : Nat} :
     (l.take n).replace a b = (l.replace a b).take n := by
   induction l generalizing n with
@@ -2868,7 +2890,8 @@ theorem length_insert_pos {l : List α} {a : α} : 0 < (l.insert a).length := by
 theorem insert_eq {l : List α} {a : α} : l.insert a = if a ∈ l then l else a :: l := by
   simp [List.insert]
 
-theorem getElem?_insert_zero (l : List α) (a : α) : (l.insert a)[0]? = if a ∈ l then l[0]? else some a := by
+theorem getElem?_insert_zero (l : List α) (a : α) :
+    (l.insert a)[0]? = if a ∈ l then l[0]? else some a := by
   simp only [insert_eq]
   split <;> simp
 
@@ -2912,6 +2935,14 @@ theorem insert_append {l₁ l₂ : List α} {a : α} :
   simp only [insert_eq, mem_append]
   (repeat split) <;> simp_all
 
+theorem insert_append_of_mem_left {l₁ l₂ : List α} (h : a ∈ l₂) :
+    (l₁ ++ l₂).insert a = l₁ ++ l₂ := by
+  simp [insert_append, h]
+
+theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂) :
+    (l₁ ++ l₂).insert a = l₁.insert a ++ l₂ := by
+  simp [insert_append, h]
+
 @[simp] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
   cases n <;> simp_all
 
@@ -2922,39 +2953,6 @@ theorem insert_append {l₁ l₂ : List α} {a : α} :
 
 end insert
 
-/-! ### lookup -/
-section lookup
-variable [BEq α] [LawfulBEq α]
-
-@[simp] theorem lookup_cons_self  {k : α} : ((k,b)::es).lookup k = some b := by
-  simp [lookup_cons]
-
-theorem lookup_replicate {k : α} :
-    (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    simp only [replicate_succ, lookup_cons]
-    split <;> simp_all
-
-theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
-    (replicate n (a, b)).lookup k = if k == a then some b else none := by
-  simp [lookup_replicate, Nat.ne_of_gt h]
-
-theorem lookup_replicate_self {a : α} :
-    (replicate n (a, b)).lookup a = if n = 0 then none else some b := by
-  simp [lookup_replicate]
-
-@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
-    (replicate n (a, b)).lookup a = some b := by
-  simp [lookup_replicate_self, Nat.ne_of_gt h]
-
-@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
-    (replicate n (a, b)).lookup k = none := by
-  simp_all [lookup_replicate]
-
-end lookup
-
 /-! ## Logic -/
 
 /-! ### any / all -/
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 468b17933369..eee93f1d995d 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -436,6 +436,18 @@ theorem take_takeWhile {l : List α} (p : α → Bool) n :
   | nil => rfl
   | cons h t ih => by_cases p h <;> simp_all
 
+theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool} (h : p a = p b) :
+    (l.takeWhile p).replace a b = (l.replace a b).takeWhile p := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [takeWhile_cons, replace_cons]
+    split <;> rename_i h₁ <;> split <;> rename_i h₂
+    · simp_all
+    · simp [replace_cons, h₂, takeWhile_cons, h₁, ih]
+    · simp_all
+    · simp_all
+
 /-! ### splitAt -/
 
 @[simp] theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n) := by

From 74cf53f2b1cbe87882f3d8263c359e53a07d7a9b Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 5 Sep 2024 12:44:16 -0700
Subject: [PATCH 02/11] fix: preserve order of overapplied arguments in
 `elab_as_elim` procedure (#5266)

When an eliminator was overapplied with more than one additional
argument, elaboration produced an incorrect term because the list of
processed arguments was being reversed. Now these arguments are not
reversed.
---
 src/Lean/Elab/App.lean         | 12 ++++++++----
 tests/lean/run/elabAsElim.lean |  7 +++++++
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index ce07129b45f9..a9b0f9ff865b 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -761,9 +761,12 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr) : MetaM Expr := do
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
     return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
 
-/-- If the eliminator is over-applied, we "revert" the extra arguments. -/
-def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=
-  args.foldrM (init := (f, expectedType)) fun arg (f, expectedType) => do
+/--
+If the eliminator is over-applied, we "revert" the extra arguments.
+Returns the function with the reverted arguments applied and the new generalized expected type.
+-/
+def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) := do
+  let (xs, expectedType) ← args.foldrM (init := ([], expectedType)) fun arg (xs, expectedType) => do
     let val ←
       match arg with
       | .expr val => pure val
@@ -772,7 +775,8 @@ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (E
     let expectedTypeBody ← kabstract expectedType val
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let valType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType val))
-    return (mkApp f val, mkForall (← mkFreshBinderName) BinderInfo.default valType expectedTypeBody)
+    return (val :: xs, mkForall (← mkFreshBinderName) BinderInfo.default valType expectedTypeBody)
+  return (xs.foldl .app f, expectedType)
 
 /--
 Construct the resulting application after all discriminants have been elaborated, and we have
diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean
index 80347f79c22e..2b950aa6e7cf 100644
--- a/tests/lean/run/elabAsElim.lean
+++ b/tests/lean/run/elabAsElim.lean
@@ -186,3 +186,10 @@ example (h : False) : Nat := False.rec (fun _ => Nat) h
 example (h : False) : Nat := False.rec _ h
 example (h : False) : Nat := h.rec
 example (h : False) : Nat := h.rec _
+
+/-!
+Check that the overapplied arguments given to the eliminator are not permuted.
+In this example, `h0` and `h1` used to be reversed, leading to a kernel typechecking error.
+-/
+example (n : Nat) (h0 : n ≠ 0) (h1 : n ≠ 1) : n - 2 ≠ n - 1 :=
+  Nat.recOn n (by simp) (by rintro (_ | _) <;> simp) h0 h1

From f18ecd4493f78b51aebffe2153318cf0a49799a1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 09:32:41 +1000
Subject: [PATCH 03/11] chore: protect some Nat bitwise theorems (#5267)

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 34 +++++++++++++--------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 64cc6fe86e65..d6bff78bdb30 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -440,26 +440,26 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
   simp [HAnd.hAnd, AndOp.and, land, testBit_bitwise ]
 
 
-@[simp] theorem and_self (x : Nat) : x &&& x = x := by
+@[simp] protected theorem and_self (x : Nat) : x &&& x = x := by
    apply Nat.eq_of_testBit_eq
    simp
 
-theorem and_comm (x y : Nat) : x &&& y = y &&& x := by
+protected theorem and_comm (x y : Nat) : x &&& y = y &&& x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_comm]
 
-theorem and_assoc (x y z : Nat) : (x &&& y) &&& z = x &&& (y &&& z) := by
+protected theorem and_assoc (x y z : Nat) : (x &&& y) &&& z = x &&& (y &&& z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_assoc]
 
 instance : Std.Associative (α := Nat) (· &&& ·) where
-  assoc := and_assoc
+  assoc := Nat.and_assoc
 
 instance : Std.Commutative (α := Nat) (· &&& ·) where
-  comm := and_comm
+  comm := Nat.and_comm
 
 instance : Std.IdempotentOp (α := Nat) (· &&& ·) where
-  idempotent := and_self
+  idempotent := Nat.and_self
 
 theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n := by
   apply lt_pow_two_of_testBit
@@ -504,15 +504,15 @@ theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 := by
 @[simp] theorem testBit_or (x y i : Nat) : (x ||| y).testBit i = (x.testBit i || y.testBit i) := by
   simp [HOr.hOr, OrOp.or, lor, testBit_bitwise ]
 
-@[simp] theorem or_self (x : Nat) : x ||| x = x := by
+@[simp] protected theorem or_self (x : Nat) : x ||| x = x := by
    apply Nat.eq_of_testBit_eq
    simp
 
-theorem or_comm (x y : Nat) : x ||| y = y ||| x := by
+protected theorem or_comm (x y : Nat) : x ||| y = y ||| x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_comm]
 
-theorem or_assoc (x y z : Nat) : (x ||| y) ||| z = x ||| (y ||| z) := by
+protected theorem or_assoc (x y z : Nat) : (x ||| y) ||| z = x ||| (y ||| z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_assoc]
 
@@ -533,13 +533,13 @@ theorem or_and_distrib_right (x y z : Nat) : (x &&& y) ||| z = (x ||| z) &&& (y
    simp [Bool.or_and_distrib_right]
 
 instance : Std.Associative (α := Nat) (· ||| ·) where
-  assoc := or_assoc
+  assoc := Nat.or_assoc
 
 instance : Std.Commutative (α := Nat) (· ||| ·) where
-  comm := or_comm
+  comm := Nat.or_comm
 
 instance : Std.IdempotentOp (α := Nat) (· ||| ·) where
-  idempotent := or_self
+  idempotent := Nat.or_self
 
 instance : Std.LawfulCommIdentity (α := Nat) (· ||| ·) 0 where
   left_id := zero_or
@@ -571,23 +571,23 @@ theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
    apply Nat.eq_of_testBit_eq
    simp
 
-@[simp] theorem xor_self (x : Nat) : x ^^^ x = 0 := by
+@[simp] protected theorem xor_self (x : Nat) : x ^^^ x = 0 := by
    apply Nat.eq_of_testBit_eq
    simp
 
-theorem xor_comm (x y : Nat) : x ^^^ y = y ^^^ x := by
+protected theorem xor_comm (x y : Nat) : x ^^^ y = y ^^^ x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.xor_comm]
 
-theorem xor_assoc (x y z : Nat) : (x ^^^ y) ^^^ z = x ^^^ (y ^^^ z) := by
+protected theorem xor_assoc (x y z : Nat) : (x ^^^ y) ^^^ z = x ^^^ (y ^^^ z) := by
    apply Nat.eq_of_testBit_eq
    simp
 
 instance : Std.Associative (α := Nat) (· ^^^ ·) where
-  assoc := xor_assoc
+  assoc := Nat.xor_assoc
 
 instance : Std.Commutative (α := Nat) (· ^^^ ·) where
-  comm := xor_comm
+  comm := Nat.xor_comm
 
 instance : Std.LawfulCommIdentity (α := Nat) (· ^^^ ·) 0 where
   left_id := zero_xor

From 7a6fa85ed1ed529cc110d0f3c1a204cc64f47409 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 09:45:14 +1000
Subject: [PATCH 04/11] chore: fix binders on ite_eq_left_iff (#5268)

---
 src/Init/PropLemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index d363a35df048..1b49ab341a7c 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -640,7 +640,7 @@ attribute [local simp] Decidable.imp_iff_left_iff
 @[simp] theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by
   split <;> simp_all
 
-@[simp] theorem ite_eq_left_iff {p : Prop} [Decidable p] (x y : α) : (if p then x else y) = x ↔ ¬ p → y = x := by
+@[simp] theorem ite_eq_left_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = x ↔ ¬ p → y = x := by
   split <;> simp_all
 
 @[simp] theorem ite_eq_right_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y ↔ p → x = y := by

From c8c35ad3b9c6d3a07081f87a7c845bad9f29d49d Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 10:23:07 +1000
Subject: [PATCH 05/11] chore: missing lemma about Fin.ofNat' (#5250)

---
 src/Init/Data/Fin/Lemmas.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index fab873d935ea..242a19e0ca90 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -54,6 +54,11 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
   (Fin.ofNat' a is_pos).val = a % n := rfl
 
+@[simp] theorem ofNat'_val_eq_self (x : Fin n) (h) : (Fin.ofNat' x h) = x := by
+  ext
+  rw [val_ofNat', Nat.mod_eq_of_lt]
+  exact x.2
+
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
   rfl
 

From 3ec55d3d498ce361f5886afee516d16df5cbd6fc Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 10:43:38 +1000
Subject: [PATCH 06/11] chore: Nat.testBit_add_one should not be a global simp
 lemma (#5262)

---
 src/Init/Data/BitVec/Lemmas.lean      | 4 ++--
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 8 +++++++-
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 3ee9b34ee30b..a537d407079c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1391,14 +1391,14 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
   cases b
   · simp
   · rintro (_ | i)
-    <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right]
+    <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right, Nat.testBit_add_one]
 
 theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
     (concat x b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1) := by
   simp only [concat, getLsbD, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
   cases i
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
-  · simp [Nat.div_eq_of_lt b.toNat_lt]
+  · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
 @[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
   simp [getLsbD_concat]
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index d6bff78bdb30..4610909acdcd 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -96,7 +96,13 @@ theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 
-@[simp] theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by
+/--
+Depending on use cases either `testBit_add_one` or `testBit_div_two`
+may be more useful as a `simp` lemma, so neither is a global `simp` lemma.
+-/
+-- We turn `testBit_add_one` on as a `local simp` for this file.
+@[local simp]
+theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 

From eba0cbaeb0f70473aed05541b7ba066ad8492e23 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 19:28:51 +1000
Subject: [PATCH 07/11] chore: remove HashMap's duplicated Pairwise and Sublist
 (#5269)

---
 .../DHashMap/Internal/List/Associative.lean   | 11 ++-
 src/Std/Data/DHashMap/Internal/List/Defs.lean |  7 +-
 .../Data/DHashMap/Internal/List/Pairwise.lean | 64 ------------
 .../Data/DHashMap/Internal/List/Sublist.lean  | 97 -------------------
 4 files changed, 8 insertions(+), 171 deletions(-)
 delete mode 100644 src/Std/Data/DHashMap/Internal/List/Pairwise.lean
 delete mode 100644 src/Std/Data/DHashMap/Internal/List/Sublist.lean

diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 3e71db3b1fe1..a3a7fa09bd89 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -6,7 +6,8 @@ Authors: Markus Himmel
 prelude
 import Init.Data.BEq
 import Init.Data.Nat.Simproc
-import Std.Data.DHashMap.Internal.List.Pairwise
+import Init.Data.List.Perm
+import Std.Data.DHashMap.Internal.List.Defs
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -22,7 +23,7 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : α → Type w}
 
-open List (Perm)
+open List (Perm Sublist pairwise_cons erase_sublist filter_sublist)
 
 namespace Std.DHashMap.Internal.List
 
@@ -689,7 +690,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     rw [eraseKey_cons]
     cases k' == k
     · simpa
-    · simpa using Sublist.cons_right Sublist.refl
+    · simp
 
 theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length := by
@@ -753,7 +754,7 @@ open List
 
 theorem DistinctKeys.perm_keys [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)}
     (h : Perm (keys l') (keys l)) : DistinctKeys l → DistinctKeys l'
-  | ⟨h'⟩ => ⟨h'.perm BEq.symm_false h.symm⟩
+  | ⟨h'⟩ => ⟨h'.perm h.symm BEq.symm_false⟩
 
 theorem DistinctKeys.perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)}
     (h : Perm l' l) : DistinctKeys l → DistinctKeys l' :=
@@ -773,7 +774,7 @@ theorem distinctKeys_of_sublist [BEq α] {l l' : List ((a : α) × β a)} (h : S
 
 theorem DistinctKeys.of_keys_eq [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × γ a)}
     (h : keys l = keys l') : DistinctKeys l → DistinctKeys l' :=
-  distinctKeys_of_sublist_keys (h ▸ Sublist.refl)
+  distinctKeys_of_sublist_keys (h ▸ Sublist.refl _)
 
 theorem containsKey_iff_exists [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
     containsKey a l ↔ ∃ a' ∈ keys l, a == a' := by
diff --git a/src/Std/Data/DHashMap/Internal/List/Defs.lean b/src/Std/Data/DHashMap/Internal/List/Defs.lean
index 112cd2b20989..794d68a4e83e 100644
--- a/src/Std/Data/DHashMap/Internal/List/Defs.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Defs.lean
@@ -20,12 +20,9 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : α → Type w}
 
-namespace Std.DHashMap.Internal.List
+open List (Pairwise)
 
-/-- Internal implementation detail of the hash map -/
-def Pairwise (P : α → α → Prop) : List α → Prop
-| [] => True
-| (x::xs) => (∀ y ∈ xs, P x y) ∧ Pairwise P xs
+namespace Std.DHashMap.Internal.List
 
 /-- Internal implementation detail of the hash map -/
 def keys : List ((a : α) × β a) → List α
diff --git a/src/Std/Data/DHashMap/Internal/List/Pairwise.lean b/src/Std/Data/DHashMap/Internal/List/Pairwise.lean
deleted file mode 100644
index 38455e818a28..000000000000
--- a/src/Std/Data/DHashMap/Internal/List/Pairwise.lean
+++ /dev/null
@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Data.List.Perm
-import Std.Data.DHashMap.Internal.List.Defs
-import Std.Data.DHashMap.Internal.List.Sublist
-
-/-!
-This is an internal implementation file of the hash map. Users of the hash map should not rely on
-the contents of this file.
-
-File contents: tiny private implementation of `List.Pairwise`
--/
-
-set_option linter.missingDocs true
-set_option autoImplicit false
-
-open List (Perm)
-
-namespace Std.DHashMap.Internal.List
-
-
-universe u
-
-variable {α : Type u}
-
-@[simp]
-theorem Pairwise.nil {P : α → α → Prop} : Pairwise P [] :=
-  trivial
-
-theorem Pairwise.perm {P : α → α → Prop} (hP : ∀ {x y}, P x y → P y x) {l l' : List α}
-    (h : Perm l l') : Pairwise P l → Pairwise P l' := by
-  induction h
-  · exact id
-  · next l₁ l₂ a h ih => exact fun hx => ⟨fun y hy => hx.1 _ (h.mem_iff.2 hy), ih hx.2⟩
-  · next l₁ a a' =>
-    intro ⟨hx₁, hx₂, hx⟩
-    refine ⟨?_, ?_, hx⟩
-    · intro y hy
-      rcases List.mem_cons.1 hy with rfl|hy
-      · exact hP (hx₁ _ (List.mem_cons_self _ _))
-      · exact hx₂ _ hy
-    · exact fun y hy => hx₁ _ (List.mem_cons_of_mem _ hy)
-  · next ih₁ ih₂ => exact ih₂ ∘ ih₁
-
-theorem Pairwise.sublist {P : α → α → Prop} {l l' : List α} (h : Sublist l l') :
-    Pairwise P l' → Pairwise P l := by
-  induction h
-  · exact id
-  · next a l₁ l₂ h ih =>
-    intro ⟨hx₁, hx⟩
-    exact ⟨fun y hy => hx₁ _ (h.mem hy), ih hx⟩
-  · next a l₁ l₂ _ ih =>
-    intro ⟨_, hx⟩
-    exact ih hx
-
-theorem pairwise_cons {P : α → α → Prop} {a : α} {l : List α} :
-    Pairwise P (a::l) ↔ (∀ y ∈ l, P a y) ∧ Pairwise P l :=
-  Iff.rfl
-
-end Std.DHashMap.Internal.List
diff --git a/src/Std/Data/DHashMap/Internal/List/Sublist.lean b/src/Std/Data/DHashMap/Internal/List/Sublist.lean
deleted file mode 100644
index 2c6d1d4622e3..000000000000
--- a/src/Std/Data/DHashMap/Internal/List/Sublist.lean
+++ /dev/null
@@ -1,97 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Omega
-
-/-!
-This is an internal implementation file of the hash map. Users of the hash map should not rely on
-the contents of this file.
-
-File contents: tiny private implementation of `List.Sublist`
--/
-
-set_option linter.missingDocs true
-set_option autoImplicit false
-
-universe u v
-
-variable {α : Type u} {β : Type v}
-
-namespace Std.DHashMap.Internal.List
-
-/-- Internal implementation detail of the hash map -/
-inductive Sublist : List α → List α → Prop where
-  /-- Internal implementation detail of the hash map -/
-  | refl {l} : Sublist l l
-  /-- Internal implementation detail of the hash map -/
-  | cons {a} {l l'} : Sublist l l' → Sublist (a::l) (a::l')
-    /-- Internal implementation detail of the hash map -/
-  | cons_right {a} {l l'} : Sublist l l' → Sublist l (a::l')
-
-@[simp]
-theorem sublist_nil {l : List α} : Sublist [] l := by
-  induction l
-  · exact .refl
-  · exact .cons_right ‹_›
-
-theorem Sublist.length_le {l₁ l₂ : List α} (h : Sublist l₁ l₂) : l₁.length ≤ l₂.length := by
-  induction h <;> simp_all <;> omega
-
-theorem Sublist.of_cons_left {l₁ l₂ : List α} {a : α} (h : Sublist (a::l₁) l₂) : Sublist l₁ l₂ := by
-  cases h
-  · exact .cons_right .refl
-  · exact .cons_right ‹_›
-  · next h t ih => exact .cons_right (Sublist.of_cons_left ‹_›)
-
-@[simp]
-theorem Sublist.cons_iff {a : α} {l₁ l₂ : List α} : Sublist (a::l₁) (a::l₂) ↔ Sublist l₁ l₂ := by
-  refine ⟨fun h => ?_, .cons⟩
-  cases h
-  · exact .refl
-  · exact ‹_›
-  · next h =>
-    cases l₂
-    · simpa using h.length_le
-    · next b t => exact Sublist.of_cons_left h
-
-theorem Sublist.map (f : α → β) {l₁ l₂ : List α} (h : Sublist l₁ l₂) :
-    Sublist (l₁.map f) (l₂.map f) := by
-  induction h
-  · exact .refl
-  · exact .cons ‹_›
-  · exact .cons_right ‹_›
-
-theorem Sublist.mem {l₁ l₂ : List α} (h : Sublist l₁ l₂) {a : α} : a ∈ l₁ → a ∈ l₂ := by
-  induction h
-  · exact id
-  · next ih =>
-    simp only [List.mem_cons]
-    rintro (ha|ha)
-    · exact Or.inl ha
-    · exact Or.inr (ih ha)
-  · next ih =>
-    simp only [List.mem_cons]
-    exact fun ha => Or.inr (ih ha)
-
-theorem erase_sublist [BEq α] (l : List α) (a : α) : Sublist (l.erase a) l := by
-  induction l
-  · simp
-  · next h t ih =>
-    simp only [List.erase_cons]
-    split
-    · exact .cons_right .refl
-    · exact .cons ih
-
-theorem filter_sublist (l : List α) {f : α → Bool} : Sublist (l.filter f) l := by
-  induction l
-  · simp
-  · next h t ih =>
-    simp only [List.filter_cons]
-    split
-    · exact .cons ih
-    · exact .cons_right ih
-
-end Std.DHashMap.Internal.List

From 943dec48c4c587f0d0810fbec5394d2463f3fd43 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 21:39:29 +1000
Subject: [PATCH 08/11] feat: remove @[simp] from Option.pmap/pbind and add
 simp lemmas (#5272)

---
 src/Init/Data/Option/Instances.lean |  4 +--
 src/Init/Data/Option/Lemmas.lean    | 48 ++++++++++++++++++++++++++++-
 2 files changed, 49 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean
index 865a958474eb..cfce9a4038b3 100644
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@@ -55,7 +55,7 @@ partial function defined on `a : α` giving an `Option β`, where `some a = x`,
 then `pbind x f h` is essentially the same as `bind x f`
 but is defined only when all `x = some a`, using the proof to apply `f`.
 -/
-@[simp, inline]
+@[inline]
 def pbind : ∀ x : Option α, (∀ a : α, a ∈ x → Option β) → Option β
   | none, _ => none
   | some a, f => f a rfl
@@ -65,7 +65,7 @@ Partial map. If `f : Π a, p a → β` is a partial function defined on `a : α`
 then `pmap f x h` is essentially the same as `map f x` but is defined only when all members of `x`
 satisfy `p`, using the proof to apply `f`.
 -/
-@[simp, inline] def pmap {p : α → Prop} (f : ∀ a : α, p a → β) :
+@[inline] def pmap {p : α → Prop} (f : ∀ a : α, p a → β) :
     ∀ x : Option α, (∀ a, a ∈ x → p a) → Option β
   | none, _ => none
   | some a, H => f a (H a rfl)
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index efc26456b68e..9cf7349bd643 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -11,7 +11,11 @@ import Init.Ext
 
 namespace Option
 
-theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = a := .rfl
+theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
+
+@[simp] theorem mem_some {a b : α} : a ∈ some b ↔ a = b := by simp [mem_iff, eq_comm]
+
+theorem mem_some_self (a : α) : a ∈ some a := mem_some.2 rfl
 
 theorem some_ne_none (x : α) : some x ≠ none := nofun
 
@@ -395,4 +399,46 @@ section ite
 
 end ite
 
+/-! ### pbind -/
+
+@[simp] theorem pbind_none : pbind none f = none := rfl
+@[simp] theorem pbind_some : pbind (some a) f = f a (mem_some_self a) := rfl
+
+@[simp] theorem map_pbind {o : Option α} {f : (a : α) → a ∈ o → Option β} {g : β → γ} :
+    (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
+  cases o <;> simp
+
+@[congr] theorem pbind_congr {o o' : Option α} (ho : o = o')
+    {f : (a : α) → a ∈ o → Option β} {g : (a : α) → a ∈ o' → Option β}
+    (hf : ∀ a h, f a (ho ▸ h) = g a h) : o.pbind f = o'.pbind g := by
+  subst ho
+  exact (funext fun a => funext fun h => hf a h) ▸ Eq.refl (o.pbind f)
+
+/-! ### pmap -/
+
+@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+    pmap f none h = none := rfl
+
+@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h}:
+    pmap f (some a) h = f a (h a (mem_some_self a)) := rfl
+
+@[simp] theorem pmap_eq_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+    pmap f o h = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem pmap_isSome {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+    (pmap f o h).isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem pmap_eq_some {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+    pmap f o h = some b ↔ ∃ (a : α) (h : p a), o = some a ∧ b = f a h := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pmap, eq_comm, some.injEq, exists_and_left, exists_eq_left']
+    constructor
+    · exact fun w => ⟨h a rfl, w⟩
+    · rintro ⟨h, rfl⟩
+      rfl
+
 end Option

From e5eea670206f99c622845d167c643a31ff3d424c Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 6 Sep 2024 21:55:50 +1000
Subject: [PATCH 09/11] chore: reverse direction of List.tail_map (#5275)

---
 src/Init/Data/List/Lemmas.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 6500c77c6416..ef102bb8fe72 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1151,18 +1151,18 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
 @[simp] theorem head?_map (f : α → β) (l : List α) : head? (map f l) = (head? l).map f := by
   cases l <;> rfl
 
-@[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
+@[simp] theorem map_tail? (f : α → β) (l : List α) : (tail? l).map (map f) = tail? (map f l) := by
   cases l <;> rfl
 
-@[simp] theorem tail_map (f : α → β) (l : List α) :
-    (map f l).tail = map f l.tail := by
+@[simp] theorem map_tail (f : α → β) (l : List α) :
+    map f l.tail = (map f l).tail := by
   cases l <;> simp_all
 
 theorem headD_map (f : α → β) (l : List α) (a : α) : headD (map f l) (f a) = f (headD l a) := by
   cases l <;> rfl
 
 theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
-    tailD (map f l) (map f l') = map f (tailD l l') := by simp
+    tailD (map f l) (map f l') = map f (tailD l l') := by simp [← map_tail?]
 
 @[simp] theorem getLast_map (f : α → β) (l : List α) (h) :
     getLast (map f l) h = f (getLast l (by simpa using h)) := by

From fcfead8cde816c28f29a3ce6fe4eaf4c015c13a7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sat, 7 Sep 2024 08:14:56 +1000
Subject: [PATCH 10/11] feat: lemmas about List.attach (#5273)

#5272 should be merged first; this contains some material from that PR.
---
 src/Init/Data/List/Attach.lean | 161 +++++++++++++++++++++++++--------
 src/Init/Data/List/Lemmas.lean |  14 +++
 2 files changed, 137 insertions(+), 38 deletions(-)

diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 0182934e8e5c..ab5ee3209722 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -55,11 +55,14 @@ theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) :
   · rfl
   · simp only [*, pmap, map]
 
-theorem pmap_congr {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂}
+theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂}
     (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
   induction l with
   | nil => rfl
-  | cons x l ih => rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)]
+  | cons x l ih =>
+    rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)]
+
+@[deprecated pmap_congr_left (since := "2024-09-06")] abbrev pmap_congr := @pmap_congr_left
 
 theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) :
     map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
@@ -74,15 +77,16 @@ theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H)
   · simp only [*, pmap, map]
 
 @[simp] theorem attach_cons (x : α) (xs : List α) :
-    (x :: xs).attach = ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by
+    (x :: xs).attach =
+      ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and]
-  apply pmap_congr
+  apply pmap_congr_left
   intros a _ m' _
   rfl
 
 theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
     pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
-  rw [attach, attachWith, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl
+  rw [attach, attachWith, map_pmap]; exact pmap_congr_left l fun _ _ _ _ => rfl
 
 theorem attach_map_coe (l : List α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
@@ -95,11 +99,13 @@ theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
   (attach_map_coe _ _).trans (List.map_id _)
 
-theorem countP_attach (l : List α) (p : α → Bool) : l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
+theorem countP_attach (l : List α) (p : α → Bool) :
+    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
   simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]
 
 @[simp]
-theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a :=
+theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) :
+    l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
 
 @[simp]
@@ -114,6 +120,11 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
     b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
   simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
 
+theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) :
+    f a (H a h) ∈ pmap f l H := by
+  rw [mem_pmap]
+  exact ⟨a, h, rfl⟩
+
 @[simp]
 theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pmap f l H) = length l := by
   induction l
@@ -125,17 +136,26 @@ theorem length_attach (L : List α) : L.attach.length = L.length :=
   length_pmap
 
 @[simp]
-theorem pmap_eq_nil {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by
+theorem pmap_eq_nil_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by
   rw [← length_eq_zero, length_pmap, length_eq_zero]
 
-theorem pmap_ne_nil {P : α → Prop} (f : (a : α) → P a → β) {xs : List α}
+theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by
   simp
 
 @[simp]
-theorem attach_eq_nil {l : List α} : l.attach = [] ↔ l = [] :=
-  pmap_eq_nil
+theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] :=
+  pmap_eq_nil_iff
+
+theorem attach_ne_nil_iff {l : List α} : l.attach ≠ [] ↔ l ≠ [] :=
+  pmap_ne_nil_iff _ _
+
+@[deprecated pmap_eq_nil_iff (since := "2024-09-06")] abbrev pmap_eq_nil := @pmap_eq_nil_iff
+@[deprecated pmap_ne_nil_iff (since := "2024-09-06")] abbrev pmap_ne_nil := @pmap_ne_nil_iff
+@[deprecated attach_eq_nil_iff (since := "2024-09-06")] abbrev attach_eq_nil := @attach_eq_nil_iff
+@[deprecated attach_ne_nil_iff (since := "2024-09-06")] abbrev attach_ne_nil := @attach_ne_nil_iff
 
+@[simp]
 theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
     (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by
   induction l generalizing n with
@@ -157,6 +177,7 @@ theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : 
   simp only [get?_eq_getElem?]
   simp [getElem?_pmap, h]
 
+@[simp]
 theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
     (hn : n < (pmap f l h).length) :
     (pmap f l h)[n] =
@@ -179,8 +200,38 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : 
   simp only [get_eq_getElem]
   simp [getElem_pmap]
 
+@[simp]
+theorem getElem?_attach {xs : List α} {i : Nat} :
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) := by
+  induction xs generalizing i with
+  | nil => simp
+  | cons x xs ih =>
+    rcases i with ⟨i⟩
+    · simp only [attach_cons, Option.pmap]
+      split <;> simp_all
+    · simp only [attach_cons, getElem?_cons_succ, getElem?_map, ih]
+      simp only [Option.pmap]
+      split <;> split <;> simp_all
+
+@[simp]
+theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
+    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem xs i (by simpa using h)⟩ := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem]
+  rw [getElem?_attach]
+  simp only [Option.pmap]
+  split <;> rename_i h' _
+  · simp at h
+    simp at h'
+    exfalso
+    exact Nat.lt_irrefl _ (Nat.lt_of_le_of_lt h' h)
+  · simp only [Option.some.injEq, Subtype.mk.injEq]
+    apply Option.some.inj
+    rw [← getElem?_eq_getElem, h']
+
 @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
-    (H : ∀ (a : α), a ∈ xs → P a) : (xs.pmap f H).head? = xs.attach.head?.map fun ⟨a, m⟩ => f a (H a m) := by
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).head? = xs.attach.head?.map fun ⟨a, m⟩ => f a (H a m) := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
@@ -194,6 +245,42 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : 
   | nil => simp at h
   | cons x xs ih => simp [head_pmap, ih]
 
+@[simp] theorem head?_attach (xs : List α) :
+    xs.attach.head? = xs.head?.pbind (fun a h => some ⟨a, mem_of_mem_head? h⟩) := by
+  cases xs <;> simp_all
+
+theorem head_attach {xs : List α} (h) :
+    xs.attach.head h = ⟨xs.head (by simpa using h), head_mem (by simpa using h)⟩ := by
+  cases xs with
+  | nil => simp at h
+  | cons x xs => simp [head_attach, h]
+
+theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
+    pmap f (pmap g l H₁) H₂ =
+      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
+        (fun a _ => H₁ a a.2) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [pmap, ih, cons.injEq, true_and]
+    ext1 i
+    simp only [getElem?_pmap, Option.pmap]
+    split <;> rename_i h _ <;> split <;> rename_i h' _
+    · rfl
+    · simp only [getElem?_attach, Option.pmap_eq_none, getElem?_eq_none_iff] at h
+      simp [getElem?_eq_none h] at h'
+    · simp only [getElem?_pmap, Option.pmap_eq_none, getElem?_eq_none_iff] at h'
+      rw [getElem?_eq_none] at h
+      simp only [reduceCtorEq] at h
+      simpa using h'
+    · simp only [getElem?_attach, Option.pmap_eq_some, exists_and_left] at h
+      simp only [getElem?_pmap, Option.pmap_eq_some, mem_cons, exists_and_left] at h'
+      obtain ⟨a, h, x, rfl⟩ := h
+      obtain ⟨a, h', x', rfl⟩ := h'
+      simp only [h, Option.some.injEq] at h'
+      subst h'
+      rfl
+
 @[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : List ι)
     (h : ∀ a ∈ l₁ ++ l₂, p a) :
     (l₁ ++ l₂).pmap f h =
@@ -212,11 +299,13 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ :
   pmap_append f l₁ l₂ _
 
 @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
-    (H : ∀ (a : α), a ∈ xs.reverse → P a) : xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
+    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
+    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
 theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
-    (H : ∀ (a : α), a ∈ xs → P a) : (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
 @[simp] theorem attach_append (xs ys : List α) :
@@ -224,33 +313,36 @@ theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, pmap_append]
   congr 1 <;>
-  exact pmap_congr _ fun _ _ _ _ => rfl
+  exact pmap_congr_left _ fun _ _ _ _ => rfl
 
-@[simp] theorem attach_reverse (xs : List α) : xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+@[simp] theorem attach_reverse (xs : List α) :
+    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
-  apply pmap_congr
+  apply pmap_congr_left
   intros
   rfl
 
-theorem reverse_attach (xs : List α) : xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+theorem reverse_attach (xs : List α) :
+    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
-  apply pmap_congr
+  apply pmap_congr_left
   intros
   rfl
 
-
+@[simp]
 theorem getLast?_attach {xs : List α} :
-    xs.attach.getLast? = match h : xs.getLast? with | none => none | some a => some ⟨a, mem_of_getLast?_eq_some h⟩ := by
-  rw [getLast?_eq_head?_reverse, reverse_attach, head?_map]
-  split <;> rename_i h
-  · simp only [getLast?_eq_none_iff] at h
-    subst h
-    simp
-  · obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.mp h
-    simp
+    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast?_eq_some h⟩ := by
+  rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach]
+  simp
+
+@[simp]
+theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
+    xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩ := by
+  simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach]
 
 @[simp] theorem getLast?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
-    (H : ∀ (a : α), a ∈ xs → P a) : (xs.pmap f H).getLast? = xs.attach.getLast?.map fun ⟨a, m⟩ => f a (H a m) := by
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).getLast? = xs.attach.getLast?.map fun ⟨a, m⟩ => f a (H a m) := by
   simp only [getLast?_eq_head?_reverse]
   rw [reverse_pmap, reverse_attach, head?_map, pmap_eq_map_attach, head?_map]
   simp only [Option.map_map]
@@ -259,14 +351,7 @@ theorem getLast?_attach {xs : List α} :
 @[simp] theorem getLast_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs → P a) (h : xs.pmap f H ≠ []) :
     (xs.pmap f H).getLast h = f (xs.getLast (by simpa using h)) (H _ (getLast_mem _)) := by
-  simp only [getLast_eq_iff_getLast_eq_some, getLast?_pmap, Option.map_eq_some', Subtype.exists]
-  refine ⟨xs.getLast (by simpa using h), by simp, ?_⟩
-  simp only [getLast?_attach, and_true]
-  split <;> rename_i h'
-  · simp only [getLast?_eq_none_iff] at h'
-    subst h'
-    simp at h
-  · symm
-    simpa [getLast_eq_iff_getLast_eq_some]
+  simp only [getLast_eq_head_reverse]
+  simp only [reverse_pmap, head_pmap, head_reverse]
 
 end List
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index ef102bb8fe72..713def2ac296 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -993,6 +993,15 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
   | [], h => absurd rfl h
   | _::_, _ => .head ..
 
+theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l := by
+  intro l a h
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp at h
+    cases h
+    exact mem_cons_self a l
+
 theorem head?_concat {a : α} : (l ++ [a]).head? = l.head?.getD a := by
   cases l <;> simp
 
@@ -2374,6 +2383,11 @@ theorem getLast?_eq_head?_reverse {xs : List α} : xs.getLast? = xs.reverse.head
 theorem head?_eq_getLast?_reverse {xs : List α} : xs.head? = xs.reverse.getLast? := by
   simp
 
+theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a ∈ l := by
+  rw [getLast?_eq_head?_reverse] at h
+  rw [← mem_reverse]
+  exact mem_of_mem_head? h
+
 @[simp] theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse := by
   induction l <;> simp [*]
 

From 7432a6f01fbf0b78cfd8a983195e642ff2e65ab1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sat, 7 Sep 2024 15:29:40 +1000
Subject: [PATCH 11/11] feat: more List.attach lemmas (#5277)

---
 src/Init/Data/List/Attach.lean   | 85 +++++++++++++++++++++-----------
 src/Init/Data/Option/Lemmas.lean | 40 ++++++++++++++-
 2 files changed, 95 insertions(+), 30 deletions(-)

diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index ab5ee3209722..e2229454aff7 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -76,6 +76,11 @@ theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H)
   · rfl
   · simp only [*, pmap, map]
 
+theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
+    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
+  subst h
+  simp
+
 @[simp] theorem attach_cons (x : α) (xs : List α) :
     (x :: xs).attach =
       ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by
@@ -255,31 +260,55 @@ theorem head_attach {xs : List α} (h) :
   | nil => simp at h
   | cons x xs => simp [head_attach, h]
 
-theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
-    pmap f (pmap g l H₁) H₂ =
-      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
-        (fun a _ => H₁ a a.2) := by
+theorem attach_map {l : List α} (f : α → β) :
+    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
+  induction l <;> simp [*]
+
+theorem attach_filterMap {l : List α} {f : α → Option β} :
+    (l.filterMap f).attach = l.attach.filterMap
+      fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
   induction l with
   | nil => rfl
   | cons x xs ih =>
-    simp only [pmap, ih, cons.injEq, true_and]
-    ext1 i
-    simp only [getElem?_pmap, Option.pmap]
-    split <;> rename_i h _ <;> split <;> rename_i h' _
-    · rfl
-    · simp only [getElem?_attach, Option.pmap_eq_none, getElem?_eq_none_iff] at h
-      simp [getElem?_eq_none h] at h'
-    · simp only [getElem?_pmap, Option.pmap_eq_none, getElem?_eq_none_iff] at h'
-      rw [getElem?_eq_none] at h
-      simp only [reduceCtorEq] at h
-      simpa using h'
-    · simp only [getElem?_attach, Option.pmap_eq_some, exists_and_left] at h
-      simp only [getElem?_pmap, Option.pmap_eq_some, mem_cons, exists_and_left] at h'
-      obtain ⟨a, h, x, rfl⟩ := h
-      obtain ⟨a, h', x', rfl⟩ := h'
-      simp only [h, Option.some.injEq] at h'
-      subst h'
+    simp only [filterMap_cons, attach_cons, ih, filterMap_map]
+    split <;> rename_i h
+    · simp only [Option.pbind_eq_none_iff, reduceCtorEq, Option.mem_def, exists_false,
+        or_false] at h
+      rw [attach_congr]
+      rotate_left
+      · simp only [h]
+        rfl
+      rw [ih]
+      simp only [map_filterMap, Option.map_pbind, Option.map_some']
       rfl
+    · simp only [Option.pbind_eq_some_iff] at h
+      obtain ⟨a, h, w⟩ := h
+      simp only [Option.some.injEq] at w
+      subst w
+      simp only [Option.mem_def] at h
+      rw [attach_congr]
+      rotate_left
+      · simp only [h]
+        rfl
+      rw [attach_cons, map_cons, map_map, ih, map_filterMap]
+      congr
+      ext
+      simp
+
+theorem attach_filter {l : List α} (p : α → Bool) :
+    (l.filter p).attach = l.attach.filterMap
+      fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none := by
+  rw [attach_congr (congrFun (filterMap_eq_filter _).symm _), attach_filterMap, map_filterMap]
+  simp only [Option.guard]
+  congr
+  ext1
+  split <;> simp
+
+theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
+    pmap f (pmap g l H₁) H₂ =
+      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
+        (fun a _ => H₁ a a.2) := by
+  simp [pmap_eq_map_attach, attach_map]
 
 @[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : List ι)
     (h : ∀ a ∈ l₁ ++ l₂, p a) :
@@ -298,6 +327,13 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ :
       l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
   pmap_append f l₁ l₂ _
 
+@[simp] theorem attach_append (xs ys : List α) :
+    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_left ys h⟩) ++
+      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by
+  simp only [attach, attachWith, pmap, map_pmap, pmap_append]
+  congr 1 <;>
+  exact pmap_congr_left _ fun _ _ _ _ => rfl
+
 @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
@@ -308,13 +344,6 @@ theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp] theorem attach_append (xs ys : List α) :
-    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_left ys h⟩) ++
-      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by
-  simp only [attach, attachWith, pmap, map_pmap, pmap_append]
-  congr 1 <;>
-  exact pmap_congr_left _ fun _ _ _ _ => rfl
-
 @[simp] theorem attach_reverse (xs : List α) :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 9cf7349bd643..ed5af61eb234 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -414,6 +414,42 @@ end ite
   subst ho
   exact (funext fun a => funext fun h => hf a h) ▸ Eq.refl (o.pbind f)
 
+theorem pbind_eq_none_iff {o : Option α} {f : (a : α) → a ∈ o → Option β} :
+    o.pbind f = none ↔ o = none ∨ ∃ a h, f a h = none := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pbind_some, reduceCtorEq, mem_def, some.injEq, false_or]
+    constructor
+    · intro h
+      exact ⟨a, rfl, h⟩
+    · rintro ⟨a, rfl, h⟩
+      exact h
+
+theorem pbind_isSome {o : Option α} {f : (a : α) → a ∈ o → Option β} :
+    (o.pbind f).isSome = ∃ a h, (f a h).isSome := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pbind_some, mem_def, some.injEq, eq_iff_iff]
+    constructor
+    · intro h
+      exact ⟨a, rfl, h⟩
+    · rintro ⟨a, rfl, h⟩
+      exact h
+
+theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → a ∈ o → Option β} {b : β} :
+    o.pbind f = some b ↔ ∃ a h, f a h = some b := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pbind_some, mem_def, some.injEq]
+    constructor
+    · intro h
+      exact ⟨a, rfl, h⟩
+    · rintro ⟨a, rfl, h⟩
+      exact h
+
 /-! ### pmap -/
 
 @[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
@@ -422,7 +458,7 @@ end ite
 @[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h}:
     pmap f (some a) h = f a (h a (mem_some_self a)) := rfl
 
-@[simp] theorem pmap_eq_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp] theorem pmap_eq_none_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f o h = none ↔ o = none := by
   cases o <;> simp
 
@@ -430,7 +466,7 @@ end ite
     (pmap f o h).isSome = o.isSome := by
   cases o <;> simp
 
-@[simp] theorem pmap_eq_some {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+@[simp] theorem pmap_eq_some_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
     pmap f o h = some b ↔ ∃ (a : α) (h : p a), o = some a ∧ b = f a h := by
   cases o with
   | none => simp