fix merge conflict

add lemmas used by HumanEval43 and HumanEval110

add required lemmas

fix test

cleanups

improvements

revert some changes

...

cleanups

ofFn_getElem

remove int lemmas

gcm

add grind pattern

better namespace hygiene

remove grind annotations on inequalities

deprecate forall_getElem

use implicit list/array/vector parameter

cleanups

poke

src/Init/Core.lean

@@ -2473,7 +2473,7 @@ class IdempotentOp (op : α → α → α) : Prop where
   idempotent : (x : α) → op x x = x
 
 /--
-`LeftIdentify op o` indicates `o` is a left identity of `op`.
+`LeftIdentity op o` indicates `o` is a left identity of `op`.
 
 This class does not require a proof that `o` is an identity, and
 is used primarily for inferring the identity using class resolution.
@@ -2481,7 +2481,7 @@ is used primarily for inferring the identity using class resolution.
 class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 
 /--
-`LawfulLeftIdentify op o` indicates `o` is a verified left identity of
+`LawfulLeftIdentity op o` indicates `o` is a verified left identity of
 `op`.
 -/
 class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
@@ -2489,7 +2489,7 @@ class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extend
   left_id : ∀ a, op o a = a
 
 /--
-`RightIdentify op o` indicates `o` is a right identity `o` of `op`.
+`RightIdentity op o` indicates `o` is a right identity `o` of `op`.
 
 This class does not require a proof that `o` is an identity, and is used
 primarily for inferring the identity using class resolution.
@@ -2497,7 +2497,7 @@ primarily for inferring the identity using class resolution.
 class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 
 /--
-`LawfulRightIdentify op o` indicates `o` is a verified right identity of
+`LawfulRightIdentity op o` indicates `o` is a verified right identity of
 `op`.
 -/
 class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where

src/Init/Data/Array/Count.lean

@@ -9,6 +9,7 @@ prelude
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
+import Init.Grind.Util
 
 public section
 
@@ -92,6 +93,18 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   rcases xs with ⟨xs⟩
   simp
 
+/-- This lemma is only relevant for `grind`. -/
+@[grind ←=]
+theorem _root_.Std.Internal.Array.countP_eq_zero_of_forall {xs : Array α} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
+  countP_eq_zero.mpr h
+
+/-- This lemma is only relevant for `grind`. -/
+theorem _root_.Std.Internal.Array.not_of_countP_eq_zero_of_mem {xs : Array α} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
+   countP_eq_zero.mp h _ h'
+
+grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
+  guard xs.countP p = 0
+
 @[simp] theorem countP_eq_size {p} : countP p xs = xs.size ↔ ∀ a ∈ xs, p a := by
   rcases xs with ⟨xs⟩
   simp

src/Init/Data/Array/Lemmas.lean

@@ -482,9 +482,18 @@ theorem mem_iff_getElem {a} {xs : Array α} : a ∈ xs ↔ ∃ (i : Nat) (h : i
 theorem mem_iff_getElem? {a} {xs : Array α} : a ∈ xs ↔ ∃ i : Nat, xs[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
+theorem exists_mem_iff_exists_getElem {P : α → Prop} {xs : Array α} :
+    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ hi, P (xs[i]) := by
+  cases xs; simp [List.exists_mem_iff_exists_getElem]
+
+theorem forall_mem_iff_forall_getElem {P : α → Prop} {xs : Array α} :
+    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) hi, P (xs[i]) := by
+  cases xs; simp [List.forall_mem_iff_forall_getElem]
+
+@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {xs : Array α} {p : α → Prop} :
     (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a := by
-  cases xs; simp [List.forall_getElem]
+  exact forall_mem_iff_forall_getElem.symm
 
 /-! ### isEmpty -/
 

src/Init/Data/Array/OfFn.lean

@@ -53,6 +53,11 @@ theorem ofFn_succ' {f : Fin (n+1) → α} :
   apply Array.toList_inj.mp
   simp [List.ofFn_succ]
 
+@[simp]
+theorem ofFn_getElem {xs : Array α} :
+    Array.ofFn (fun i : Fin xs.size => xs[i.val]) = xs := by
+  ext <;> simp
+
 @[simp]
 theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]
@@ -67,6 +72,12 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
+@[simp, grind =]
+theorem map_ofFn {f : Fin n → α} {g : α → β} :
+    (Array.ofFn f).map g = Array.ofFn (g ∘ f) := by
+  apply Array.ext_getElem?
+  simp [Array.getElem?_ofFn]
+
 /-! ### ofFnM -/
 
 /-- Construct (in a monadic context) an array by applying a monadic function to each index. -/

src/Init/Data/List/Count.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Sublist
+import Init.Grind.Util
 
 public section
 
@@ -97,6 +98,18 @@ theorem countP_le_length : countP p l ≤ l.length := by
 @[simp] theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
   simp only [countP_eq_length_filter, length_eq_zero_iff, filter_eq_nil_iff]
 
+/-- This lemma is only relevant for `grind`. -/
+@[grind ←=]
+theorem _root_.Std.Internal.List.countP_eq_zero_of_forall {xs : List α} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
+  countP_eq_zero.mpr h
+
+/-- This lemma is only relevant for `grind`. -/
+theorem _root_.Std.Internal.List.not_of_countP_eq_zero_of_mem {xs : List α} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
+   countP_eq_zero.mp h _ h'
+
+grind_pattern Std.Internal.List.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
+  guard xs.countP p = 0
+
 @[simp] theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by
   rw [countP_eq_length_filter, length_filter_eq_length_iff]
 

src/Init/Data/List/Lemmas.lean

@@ -482,25 +482,28 @@ theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (i : Nat) (h : i < l
 theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
+theorem exists_mem_iff_exists_getElem {P : α → Prop} {l : List α} :
+    (∃ x ∈ l, P x) ↔ ∃ (i : Nat), ∃ hi, P (l[i]) := by
+  simp only [mem_iff_getElem]
+  apply Iff.intro
+  · rintro ⟨_, ⟨i, hi, rfl⟩, hP⟩
+    exact ⟨i, hi, hP⟩
+  · rintro ⟨i, hi, hP⟩
+    exact ⟨_, ⟨i, hi, rfl⟩, hP⟩
+
+theorem forall_mem_iff_forall_getElem {P : α → Prop} {l : List α} :
+    (∀ x ∈ l, P x) ↔ ∀ (i : Nat) hi, P (l[i]) := by
+  simp only [mem_iff_getElem]
+  apply Iff.intro
+  · intro h i hi
+    exact h l[i] ⟨i, hi, rfl⟩
+  · rintro h _ ⟨i, hi, rfl⟩
+    exact h i hi
+
+@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {l : List α} {p : α → Prop} :
-    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a := by
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp only [length_cons, mem_cons, forall_eq_or_imp]
-    constructor
-    · intro w
-      constructor
-      · exact w 0 (by simp)
-      · apply ih.1
-        intro n h
-        simpa using w (n+1) (Nat.add_lt_add_right h 1)
-    · rintro ⟨h, w⟩
-      rintro (_ | n) h
-      · simpa
-      · apply w
-        simp only [getElem_cons_succ]
-        exact getElem_mem (lt_of_succ_lt_succ h)
+    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a :=
+  forall_mem_iff_forall_getElem.symm
 
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
     elem a l = l.contains a := by

src/Init/Data/List/MinMax.lean

@@ -47,7 +47,7 @@ theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = some (foldl min x
   cases xs <;> simp [min?]
 
 @[simp, grind =]
-public theorem isSome_min?_iff {xs : List α} [Min α] : xs.min?.isSome ↔ xs ≠ [] := by
+public theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [min?]
 
 @[grind .]
@@ -55,8 +55,8 @@ theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
     l.min?.isSome := by
   cases l <;> simp_all [min?_cons']
 
-theorem isSome_min?_of_ne_nil [Min α] : {l : List α} → (hl : l ≠ []) → l.min?.isSome
-  | x::xs, h => by simp [min?_cons']
+theorem isSome_min?_of_ne_nil [Min α] {l : List α} (hl : l ≠ []) : l.min?.isSome := by
+  rwa [isSome_min?_iff]
 
 theorem min?_eq_head? {α : Type u} [Min α] {l : List α}
     (h : l.Pairwise (fun a b => min a b = a)) : l.min? = l.head? := by
@@ -242,7 +242,7 @@ theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = some (foldl max x
   cases xs <;> simp [max?]
 
 @[simp, grind =]
-public theorem isSome_max?_iff {xs : List α} [Max α] : xs.max?.isSome ↔ xs ≠ [] := by
+public theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [max?]
 
 @[grind .]
@@ -250,8 +250,8 @@ theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
     l.max?.isSome := by
   cases l <;> simp_all [max?_cons']
 
-theorem isSome_max?_of_ne_nil [Max α] : {l : List α} → (hl : l ≠ []) → l.max?.isSome
-  | x::xs, h => by simp [max?_cons']
+theorem isSome_max?_of_ne_nil [Max α] {l : List α} (hl : l ≠ []) : l.max?.isSome := by
+  rwa [isSome_max?_iff]
 
 theorem max?_eq_head? {α : Type u} [Max α] {l : List α}
     (h : l.Pairwise (fun a b => max a b = a)) : l.max? = l.head? := by

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

@@ -137,6 +137,7 @@ theorem take_append {l₁ l₂ : List α} {i : Nat} :
       congr 1
       omega
 
+@[grind =]
 theorem take_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
     (l₁ ++ l₂).take i = l₁.take i := by
   simp [take_append, Nat.sub_eq_zero_of_le h]
@@ -372,7 +373,7 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
     simp only [take_succ_cons, drop_succ_cons, drop_take, take_eq_take_iff, length_drop]
     omega
 
-@[simp] theorem drop_take_self : drop i (take i l) = [] := by
+@[simp, grind =] theorem drop_take_self : drop i (take i l) = [] := by
   rw [drop_take]
   simp
 

src/Init/Data/List/OfFn.lean

@@ -100,6 +100,11 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, Nat.succ_ne_zero, reduceCtorEq]
 
+@[simp]
+theorem ofFn_getElem {xs : List α} :
+    List.ofFn (fun i : Fin xs.length => xs[i.val]) = xs := by
+  apply ext_getElem <;> simp
+
 @[simp 500, grind =]
 theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i = a := by
   constructor
@@ -109,6 +114,12 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
+@[simp, grind =]
+theorem map_ofFn {f : Fin n → α} {g : α → β} :
+    (List.ofFn f).map g = List.ofFn (g ∘ f) := by
+  apply List.ext_getElem?
+  simp [List.getElem?_ofFn]
+
 @[grind =] theorem head_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
   rw [← getElem_zero (length_ofFn ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),

src/Init/Data/List/Sublist.lean

@@ -580,7 +580,7 @@ theorem sublist_flatten_iff {L : List (List α)} {l} :
     · rintro ⟨L', rfl, h⟩
       simp only [flatten_nil, sublist_nil, flatten_eq_nil_iff]
       simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
-      exact (forall_getElem (p := (· = []))).1 h
+      exact (forall_mem_iff_forall_getElem (P := (· = []))).2 h
   | cons l' L ih =>
     simp only [flatten_cons, sublist_append_iff, ih]
     constructor
@@ -1124,9 +1124,11 @@ theorem drop_subset (i) (l : List α) : drop i l ⊆ l :=
 
 grind_pattern drop_subset => drop i l ⊆ l
 
+@[grind →]
 theorem mem_of_mem_take {l : List α} (h : a ∈ l.take i) : a ∈ l :=
   take_subset _ _ h
 
+@[grind →]
 theorem mem_of_mem_drop {i} {l : List α} (h : a ∈ l.drop i) : a ∈ l :=
   drop_subset _ _ h
 

src/Init/Data/Vector/Count.lean

@@ -70,6 +70,18 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   cases xs
   simp
 
+/-- This lemma is only relevant for `grind`. -/
+@[grind ←=]
+theorem _root_.Std.Internal.Vector.countP_eq_zero_of_forall {xs : Vector α n} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
+  countP_eq_zero.mpr h
+
+/-- This lemma is only relevant for `grind`. -/
+theorem _root_.Std.Internal.Vector.not_of_countP_eq_zero_of_mem {xs : Vector α n} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
+   countP_eq_zero.mp h _ h'
+
+grind_pattern Std.Internal.Vector.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
+  guard xs.countP p = 0
+
 @[simp] theorem countP_eq_size {p} {xs : Vector α n} : countP p xs = n ↔ ∀ a ∈ xs, p a := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -87,6 +99,7 @@ theorem boole_getElem_le_countP {p : α → Bool} {xs : Vector α n} (h : i < n)
   rcases xs with ⟨xs, rfl⟩
   simp [Array.boole_getElem_le_countP]
 
+@[grind =]
 theorem countP_set {p : α → Bool} {xs : Vector α n} {a : α} (h : i < n) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Lemmas.lean

@@ -503,6 +503,11 @@ protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → x
 
 @[simp, grind =] theorem toList_mk : (Vector.mk xs h).toList = xs.toList := rfl
 
+@[simp, grind =]
+theorem Vector.toList_zip {as : Vector α n} {bs : Vector β n} :
+    (Vector.zip as bs).toList = List.zip as.toList bs.toList := by
+  rw [mk_zip_mk, toList_mk, Array.toList_zip, toList_toArray, toList_toArray]
+
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -513,6 +518,7 @@ protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → x
   cases xs
   simp
 
+@[grind =]
 theorem toList_append {xs : Vector α m} {ys : Vector α n} :
     (xs ++ ys).toList = xs.toList ++ ys.toList := by simp [toList]
 
@@ -1028,10 +1034,18 @@ theorem mem_iff_getElem {a} {xs : Vector α n} : a ∈ xs ↔ ∃ (i : Nat) (h :
 theorem mem_iff_getElem? {a} {xs : Vector α n} : a ∈ xs ↔ ∃ i : Nat, xs[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
+theorem exists_mem_iff_exists_getElem {P : α → Prop} {xs : Vector α n} :
+    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ hi, P (xs[i]) := by
+  cases xs; simp [*, Array.exists_mem_iff_exists_getElem]
+
+theorem forall_mem_iff_forall_getElem {P : α → Prop} {xs : Vector α n} :
+    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) hi, P (xs[i]) := by
+  cases xs; simp [*, Array.forall_mem_iff_forall_getElem]
+
+@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {xs : Vector α n} {p : α → Prop} :
-    (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.forall_getElem]
+    (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a :=
+  forall_mem_iff_forall_getElem.symm
 
 /-! ### Decidability of bounded quantifiers -/
 

src/Init/Data/Vector/OfFn.lean

@@ -37,6 +37,11 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
+@[simp, grind =]
+theorem map_ofFn {f : Fin n → α} {g : α → β} :
+    (Vector.ofFn f).map g = Vector.ofFn (g ∘ f) := by
+  simp [← Vector.toArray_inj]
+
 @[grind =] theorem back_ofFn {n} [NeZero n] {f : Fin n → α} :
     (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩ := by
   simp [back]
@@ -59,6 +64,11 @@ theorem ofFn_succ' {f : Fin (n+1) → α} :
   apply Vector.toArray_inj.mp
   simp [Array.ofFn_succ']
 
+@[simp]
+theorem ofFn_getElem {xs : Vector α n} :
+    Vector.ofFn (fun i : Fin n => xs[i.val]) = xs := by
+  ext; simp
+
 /-! ### ofFnM -/
 
 /-- Construct (in a monadic context) a vector by applying a monadic function to each index. -/

tests/lean/run/pairsSumToZero.lean

@@ -14,10 +14,6 @@ open Std Do
 
 namespace List
 
-theorem exists_mem_iff_exists_getElem (P : α → Prop) (l : List α) :
-    (∃ x ∈ l, P x) ↔ ∃ (i : Nat), ∃ hi, P (l[i]'hi) := by
-  grind [mem_iff_getElem]
-
 /--
 `l.ExistsPair P` asserts that there are indices `i` and `j` such that `i < j` and `P l[i] l[j]` is true.
 -/