finish

src/Init/Data/Array/Attach.lean

@@ -143,6 +143,12 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
   cases l
   simp [List.pmap_eq_map_attach]
 
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  cases l
+  simp [List.pmap_eq_attachWith]
+
 theorem attach_map_coe (l : Array α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   cases l
@@ -173,6 +179,12 @@ theorem mem_attach (l : Array α) : ∀ x, x ∈ l.attach
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
+@[simp]
+theorem mem_attachWith (l : Array α) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  cases l
+  simp
+
 @[simp]
 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
@@ -257,6 +269,18 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
+@[simp] theorem pmap_attach (l : Array α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  ext <;> simp
+
+@[simp] theorem pmap_attachWith (l : Array α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  ext <;> simp
+
 theorem foldl_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
   (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
@@ -344,7 +368,23 @@ theorem attach_filter {l : Array α} (p : α → Bool) :
   simp [List.attach_filter, List.map_filterMap, Function.comp_def]
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
--- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
+@[simp]
+theorem filterMap_attachWith {q : α → Prop} {l : Array α} {f : {x // q x} → Option β} (H)
+    (w : stop = (l.attachWith q H).size) :
+    (l.attachWith q H).filterMap f 0 stop = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
+  subst w
+  cases l
+  simp [Function.comp_def]
+
+@[simp]
+theorem filter_attachWith {q : α → Prop} {l : Array α} {p : {x // q x} → Bool} (H)
+    (w : stop = (l.attachWith q H).size) :
+    (l.attachWith q H).filter p 0 stop =
+      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
+  subst w
+  cases l
+  simp [Function.comp_def, List.filter_map]
 
 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₂ =
@@ -424,13 +464,13 @@ theorem reverse_attach (xs : Array α) :
 
 @[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back?_eq_some h)⟩) := by
+    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
 @[simp]
 theorem back?_attach {xs : Array α} :
-    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back?_eq_some h⟩ := by
+    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs
   simp
 

src/Init/Data/Array/Lemmas.lean

@@ -3253,9 +3253,11 @@ theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD de
 @[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
   simp [back!_eq_back?]
 
-theorem mem_of_back?_eq_some {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
   cases xs
-  simpa using List.mem_of_getLast?_eq_some (by simpa using h)
+  simpa using List.mem_of_getLast? (by simpa using h)
+
+@[deprecated mem_of_back? (since := "2024-10-21")] abbrev mem_of_back?_eq_some := @mem_of_back?
 
 theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by

src/Init/Data/List/Attach.lean

@@ -111,6 +111,14 @@ 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_left l fun _ _ _ _ => rfl
 
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  induction l with
+  | nil => rfl
+  | cons a l ih =>
+    simp [pmap, attachWith, ih]
+
 theorem attach_map_coe (l : List α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, attachWith, map_pmap]; exact pmap_eq_map _ _ _ _
@@ -136,10 +144,23 @@ theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a 
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
   | ⟨a, h⟩ => by
-    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
+    have := mem_map.1 (by rw [attach_map_subtype_val]; exact h)
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
+@[simp]
+theorem mem_attachWith (l : List α) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [ih]
+    constructor
+    · rintro (_ | _) <;> simp_all
+    · rintro (h | h)
+      · simp [← h]
+      · simp_all
+
 @[simp]
 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
@@ -266,6 +287,18 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
+@[simp] theorem pmap_attach (l : List α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  apply ext_getElem <;> simp
+
+@[simp] theorem pmap_attachWith (l : List α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  apply ext_getElem <;> simp
+
 @[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
@@ -431,7 +464,25 @@ theorem attach_filter {l : List α} (p : α → Bool) :
   split <;> simp
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
--- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
+@[simp]
+theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} → Option β} (H) :
+    (l.attachWith q H).filterMap f = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [attachWith_cons, filterMap_cons]
+    split <;> simp_all [Function.comp_def]
+
+@[simp]
+theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bool} (H) :
+    (l.attachWith q H).filter p =
+      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [attachWith_cons, filter_cons]
+    split <;> simp_all [Function.comp_def, filter_map]
 
 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₂ =
@@ -520,7 +571,7 @@ theorem reverse_attach (xs : List α) :
 
 @[simp] theorem getLast?_attachWith {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast?_eq_some h)⟩) := by
+    (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast? h)⟩) := by
   rw [getLast?_eq_head?_reverse, reverse_attachWith, head?_attachWith]
   simp
 
@@ -531,7 +582,7 @@ theorem reverse_attach (xs : List α) :
 
 @[simp]
 theorem getLast?_attach {xs : List α} :
-    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast?_eq_some h⟩ := by
+    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast? h⟩ := by
   rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach]
   simp
 

src/Init/Data/List/Lemmas.lean

@@ -2750,10 +2750,12 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
   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
+theorem mem_of_getLast? {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
 
+@[deprecated mem_of_getLast? (since := "2024-10-21")] abbrev mem_of_getLast?_eq_some := @mem_of_getLast?
+
 @[simp] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.getLast h = l.head (by simp_all) := by
   simp [getLast_eq_head_reverse]

src/Init/Data/Vector/Attach.lean

@@ -134,8 +134,6 @@ theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α →
       (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   rcases l with ⟨l, rfl⟩
   simp [Array.map_attachWith]
-  congr
-  sorry
 
 @[simp] theorem attachWith_push {a : α} {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
     (l.push a).attachWith P H =
@@ -146,8 +144,15 @@ theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α →
 theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l : Vector α n) (H) :
     pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
   rcases l with ⟨l, rfl⟩
-  simp [Array.pmap_eq_map_attach]
-  sorry
+  simp only [pmap_mk, Array.pmap_eq_map_attach, attach_mk, map_mk, eq_mk]
+  rw [Array.map_attach, Array.map_attachWith]
+  ext i hi₁ hi₂ <;> simp
+
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l : Vector α n) (H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  cases l
+  simp
 
 theorem attach_map_coe (l : Vector α n) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
@@ -179,6 +184,12 @@ theorem mem_attach (l : Vector α n) : ∀ x, x ∈ l.attach
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
+@[simp]
+theorem mem_attachWith (l : Vector α n) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
 @[simp]
 theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H b} :
     b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
@@ -225,6 +236,18 @@ theorem getElem_attach {xs : Vector α n} {i : Nat} (h : i < n) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
+@[simp] theorem pmap_attach (l : Vector α n) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  ext <;> simp
+
+@[simp] theorem pmap_attachWith (l : Vector α n) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  ext <;> simp
+
 theorem foldl_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
   (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
@@ -294,8 +317,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f
       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
   rcases l with ⟨l, rfl⟩
-  simp_all [Array.pmap_pmap]
-  sorry
+  ext <;> simp
 
 @[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ : Vector ι n) (l₂ : Vector ι m)
     (h : ∀ a ∈ l₁ ++ l₂, p a) :
@@ -313,12 +335,11 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ : Vect
   pmap_append f l₁ l₂ _
 
 @[simp] theorem attach_append (xs : Vector α n) (ys : Vector α m) :
-    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
-      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xsh⟩ := by
-  cases xs
-  cases ys
-  rw [attach_congr (List.append_toArray _ _)]
-  simp [List.attach_append, Function.comp_def]
+    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
+      ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.map_attachWith]
 
 @[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
@@ -353,12 +374,12 @@ theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr (reverse_mk ..)]
-  simp
+  simp [Array.map_attachWith]
 
 theorem reverse_attach (xs : Vector α n) :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
-  simp
+  simp [Array.map_attachWith]
 
 @[simp] theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
     (H : ∀ (a : α), a ∈ xs → P a) :
@@ -368,13 +389,13 @@ theorem reverse_attach (xs : Vector α n) :
 
 @[simp] theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back?_eq_some h)⟩) := by
+    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
 @[simp]
 theorem back?_attach {xs : Vector α n} :
-    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back?_eq_some h⟩ := by
+    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs
   simp
 
@@ -406,8 +427,8 @@ theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Vector α n) (H
     (l.pmap g H₁).countP f =
       l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
   rcases l with ⟨l, rfl⟩
-  simp
-  sorry
+  simp only [pmap_mk, countP_mk, Array.countP_pmap]
+  simp [Array.countP_eq_size_filter]
 
 /-! ## unattach
 
@@ -459,7 +480,6 @@ def unattach {α : Type _} {p : α → Prop} (l : Vector { x // p x } n) : Vecto
 @[simp] theorem getElem?_unattach {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) :
     l.unattach[i]? = l[i]?.map Subtype.val := by
   simp [unattach]
-  sorry
 
 @[simp] theorem getElem_unattach
     {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) (h : i < n) :

src/Init/Data/Vector/Lemmas.lean

@@ -779,6 +779,10 @@ theorem getElem?_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ i : Nat, l[i]?
 theorem mem_of_getElem? {l : Vector α n} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
+theorem mem_of_back? {xs : Vector α n} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+  cases xs
+  simpa using Array.mem_of_back? (by simpa using h)
+
 theorem mem_iff_getElem {a} {l : Vector α n} : a ∈ l ↔ ∃ (i : Nat) (h : i < n), l[i]'h = a :=
   ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
 
@@ -1147,6 +1151,11 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases a
   simp
 
+@[simp] theorem getElem?_map (f : α → β) (a : Vector α n) (i : Nat) :
+    (a.map f)[i]? = a[i]?.map f := by
+  cases a
+  simp
+
 /-- The empty vector maps to the empty vector. -/
 @[simp]
 theorem map_empty (f : α → β) : map f #v[] = #v[] := by