uniformize

src/Init/Data/Array/Count.lean

@@ -52,6 +52,7 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x
   rcases xs with ⟨xs⟩
   simp_all
 
+@[grind =]
 theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
   simp
 
@@ -59,10 +60,12 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
+@[grind _=_]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]
 
+@[grind =]
 theorem countP_eq_size_filter' : countP p = size ∘ filter p := by
   funext xs
   apply countP_eq_size_filter
@@ -71,7 +74,7 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   simp only [countP_eq_size_filter]
   apply size_filter_le
 
-@[simp] theorem countP_append {xs ys : Array α} : countP p (xs ++ ys) = countP p xs + countP p ys := by
+@[simp, grind =] theorem countP_append {xs ys : Array α} : countP p (xs ++ ys) = countP p xs + countP p ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp
@@ -146,7 +149,7 @@ theorem countP_flatMap {p : β → Bool} {xs : Array α} {f : α → Array β} :
   rcases xs with ⟨xs⟩
   simp [List.countP_flatMap, Function.comp_def]
 
-@[simp] theorem countP_reverse {xs : Array α} : countP p xs.reverse = countP p xs := by
+@[simp, grind =] theorem countP_reverse {xs : Array α} : countP p xs.reverse = countP p xs := by
   rcases xs with ⟨xs⟩
   simp [List.countP_reverse]
 
@@ -173,7 +176,7 @@ variable [BEq α]
   cases xs
   simp
 
-@[simp] theorem count_empty {a : α} : count a #[] = 0 := rfl
+@[simp, grind =] theorem count_empty {a : α} : count a #[] = 0 := rfl
 
 theorem count_push {a b : α} {xs : Array α} :
     count a (xs.push b) = count a xs + if b == a then 1 else 0 := by
@@ -186,21 +189,28 @@ theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
 
 theorem count_le_size {a : α} {xs : Array α} : count a xs ≤ xs.size := countP_le_size
 
+grind_pattern count_le_size => count a xs
+
+@[grind =]
+theorem count_eq_size_filter {a : α} {xs : Array α} : count a xs = (filter (· == a) xs).size := by
+  simp [count, countP_eq_size_filter]
+
 theorem count_le_count_push {a b : α} {xs : Array α} : count a xs ≤ count a (xs.push b) := by
   simp [count_push]
 
+@[grind =]
 theorem count_singleton {a b : α} : count a #[b] = if b == a then 1 else 0 := by
   simp [count_eq_countP]
 
-@[simp] theorem count_append {a : α} {xs ys : Array α} : count a (xs ++ ys) = count a xs + count a ys :=
+@[simp, grind =] theorem count_append {a : α} {xs ys : Array α} : count a (xs ++ ys) = count a xs + count a ys :=
   countP_append
 
-@[simp] theorem count_flatten {a : α} {xss : Array (Array α)} :
+@[simp, grind =] theorem count_flatten {a : α} {xss : Array (Array α)} :
     count a xss.flatten = (xss.map (count a)).sum := by
   cases xss using array₂_induction
   simp [List.count_flatten, Function.comp_def]
 
-@[simp] theorem count_reverse {a : α} {xs : Array α} : count a xs.reverse = count a xs := by
+@[simp, grind =] theorem count_reverse {a : α} {xs : Array α} : count a xs.reverse = count a xs := by
   rcases xs with ⟨xs⟩
   simp
 

src/Init/Data/Array/Lemmas.lean

@@ -89,6 +89,8 @@ theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size :=
   simp only [mem_toArray] at h
   simpa using List.length_pos_of_mem h
 
+grind_pattern size_pos_of_mem => a ∈ xs, xs.size
+
 theorem exists_mem_of_size_pos {xs : Array α} (h : 0 < xs.size) : ∃ a, a ∈ xs := by
   cases xs
   simpa using List.exists_mem_of_length_pos h

src/Init/Data/Array/Perm.lean

@@ -91,17 +91,26 @@ theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a
   simp only [perm_iff_toList_perm] at p
   simpa using p.mem_iff
 
+grind_pattern Perm.mem_iff => xs ~ ys, a ∈ xs
+grind_pattern Perm.mem_iff => xs ~ ys, a ∈ ys
+
 theorem Perm.append {xs ys as bs : Array α} (p₁ : xs ~ ys) (p₂ : as ~ bs) :
     xs ++ as ~ ys ++ bs := by
   cases xs; cases ys; cases as; cases bs
   simp only [append_toArray, perm_iff_toList_perm] at p₁ p₂ ⊢
   exact p₁.append p₂
 
+grind_pattern Perm.append => xs ~ ys, as ~ bs, xs ++ as
+grind_pattern Perm.append => xs ~ ys, as ~ bs, ys ++ bs
+
 theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
     xs.push x ~ ys.push x := by
   rw [push_eq_append_singleton]
   exact p.append .rfl
 
+grind_pattern Perm.push => xs ~ ys, xs.push x
+grind_pattern Perm.push => xs ~ ys, ys.push x
+
 theorem Perm.push_comm (x y : α) {xs ys : Array α} (p : xs ~ ys) :
     (xs.push x).push y ~ (ys.push y).push x := by
   cases xs; cases ys

src/Init/Data/Array/Range.lean

@@ -128,6 +128,16 @@ theorem erase_range' :
   simp only [← List.toArray_range', List.erase_toArray]
   simp [List.erase_range']
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [← List.toArray_range', List.count_toArray, ← List.count_range' h]
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [← List.toArray_range', List.count_toArray, ← List.count_range_1']
+
 /-! ### range -/
 
 @[grind _=_]
@@ -191,6 +201,10 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [← List.toArray_range, List.count_toArray, ← List.count_range]
 
 /-! ### zipIdx -/
 

src/Init/Data/List/Count.lean

@@ -64,8 +64,8 @@ theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l =
       · rfl
       · simp [h]
 
-@[grind =]
-theorem countP_eq_length_filter {l : List α} : countP p l = length (filter p l) := by
+@[grind _=_]  -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
+theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length := by
   induction l with
   | nil => rfl
   | cons x l ih =>
@@ -82,7 +82,7 @@ theorem countP_le_length : countP p l ≤ l.length := by
   simp only [countP_eq_length_filter]
   apply length_filter_le
 
-@[simp] theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
+@[simp, grind =] theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
   simp only [countP_eq_length_filter, filter_append, length_append]
 
 @[simp] theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by
@@ -120,10 +120,24 @@ theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ :
   simp only [countP_eq_length_filter]
   apply s.filter _ |>.length_le
 
+grind_pattern Sublist.countP_le => l₁ <+ l₂, countP p l₁
+grind_pattern Sublist.countP_le => l₁ <+ l₂, countP p l₂
+
 theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
+
+grind_pattern IsPrefix.countP_le => l₁ <+: l₂, countP p l₁
+grind_pattern IsPrefix.countP_le => l₁ <+: l₂, countP p l₂
+
 theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
+
+grind_pattern IsSuffix.countP_le => l₁ <:+ l₂, countP p l₁
+grind_pattern IsSuffix.countP_le => l₁ <:+ l₂, countP p l₂
+
 theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
 
+grind_pattern IsInfix.countP_le => l₁ <:+: l₂, countP p l₁
+grind_pattern IsInfix.countP_le => l₁ <:+: l₂, countP p l₂
+
 -- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
 
 @[grind]
@@ -174,7 +188,7 @@ theorem countP_flatMap {p : β → Bool} {l : List α} {f : α → List β} :
     countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
   rw [List.flatMap, countP_flatten, map_map]
 
-@[simp] theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
+@[simp, grind =] theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
   simp [countP_eq_length_filter, filter_reverse]
 
 theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
@@ -203,18 +217,22 @@ section count
 
 variable [BEq α]
 
-@[simp] theorem count_nil {a : α} : count a [] = 0 := rfl
+@[simp, grind =] theorem count_nil {a : α} : count a [] = 0 := rfl
 
 @[grind]
 theorem count_cons {a b : α} {l : List α} :
     count a (b :: l) = count a l + if b == a then 1 else 0 := by
   simp [count, countP_cons]
 
-@[grind =] theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
+theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
 theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
   funext l
   apply count_eq_countP
 
+@[grind =]
+theorem count_eq_length_filter {a : α} {l : List α} : count a l = (filter (· == a) l).length := by
+  simp [count, countP_eq_length_filter]
+
 @[grind]
 theorem count_tail : ∀ {l : List α} {a : α},
       l.tail.count a = l.count a - if l.head? == some a then 1 else 0
@@ -223,12 +241,28 @@ theorem count_tail : ∀ {l : List α} {a : α},
 
 theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length
 
+grind_pattern count_le_length => count a l
+
 theorem Sublist.count_le (a : α) (h : l₁ <+ l₂) : count a l₁ ≤ count a l₂ := h.countP_le
 
+grind_pattern Sublist.count_le => l₁ <+ l₂, count a l₁
+grind_pattern Sublist.count_le => l₁ <+ l₂, count a l₂
+
 theorem IsPrefix.count_le (a : α) (h : l₁ <+: l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
+
+grind_pattern IsPrefix.count_le => l₁ <+: l₂, count a l₁
+grind_pattern IsPrefix.count_le => l₁ <+: l₂, count a l₂
+
 theorem IsSuffix.count_le (a : α) (h : l₁ <:+ l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
+
+grind_pattern IsSuffix.count_le => l₁ <:+ l₂, count a l₁
+grind_pattern IsSuffix.count_le => l₁ <:+ l₂, count a l₂
+
 theorem IsInfix.count_le (a : α) (h : l₁ <:+: l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
 
+grind_pattern IsInfix.count_le => l₁ <:+: l₂, count a l₁
+grind_pattern IsInfix.count_le => l₁ <:+: l₂, count a l₂
+
 -- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`.
 
 theorem count_tail_le {a : α} {l : List α} : count a l.tail ≤ count a l :=
@@ -245,10 +279,11 @@ theorem count_singleton {a b : α} : count a [b] = if b == a then 1 else 0 := by
 @[simp, grind =] theorem count_append {a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append
 
+@[grind =]
 theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
-@[simp] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
+@[simp, grind =] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
   simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]
 
 @[grind]

src/Init/Data/List/Lemmas.lean

@@ -109,9 +109,11 @@ abbrev length_eq_zero := @length_eq_zero_iff
 theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
   length_eq_zero_iff.symm
 
-@[grind →] theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
+theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
   | _::_, _ => Nat.zero_lt_succ _
 
+grind_pattern length_pos_of_mem => a ∈ l, length l
+
 theorem exists_mem_of_length_pos : ∀ {l : List α}, 0 < length l → ∃ a, a ∈ l
   | _::_, _ => ⟨_, .head ..⟩
 

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

@@ -60,6 +60,25 @@ theorem count_replace [BEq α] [LawfulBEq α] {a b c : α} {l : List α} :
       if l.contains a then l.count c + (if b == c then 1 else 0) - (if a == c then 1 else 0) else l.count c := by
   simp [count_eq_countP, countP_replace]
 
+@[grind =] theorem count_insert [BEq α] [LawfulBEq α] {a b : α} {l : List α} :
+    count a (List.insert b l) = max (count a l) (if b == a then 1 else 0) := by
+  simp only [List.insert, contains_eq_mem, decide_eq_true_eq, beq_iff_eq]
+  split <;> rename_i h
+  · split <;> rename_i h'
+    · rw [Nat.max_def]
+      simp only [beq_iff_eq] at h'
+      split
+      · have := List.count_pos_iff.mpr (h' ▸ h)
+        omega
+      · rfl
+    · simp [h']
+  · rw [count_cons]
+    split <;> rename_i h'
+    · simp only [beq_iff_eq] at h'
+      rw [count_eq_zero.mpr (h' ▸ h)]
+      simp [h']
+    · simp
+
 /--
 The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list,
 minus the difference in the lengths.

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

@@ -158,6 +158,26 @@ theorem erase_range' :
       simp [p]
       omega
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [(nodup_range' step h).count]
+  simp only [mem_range']
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [count_range' (by simp)]
+  split <;> rename_i h
+  · obtain ⟨i, h, rfl⟩ := h
+    simp [h]
+  · simp at h
+    rw [if_neg]
+    simp only [not_and, Nat.not_lt]
+    intro w
+    specialize h (a - s)
+    omega
+
 /-! ### range -/
 
 theorem reverse_range' : ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1 - ·) (range n)
@@ -200,6 +220,12 @@ theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [range_eq_range', count_range_1']
+  simp
+
 /-! ### iota -/
 
 section

src/Init/Data/List/Pairwise.lean

@@ -279,7 +279,11 @@ theorem nodup_nil : @Nodup α [] :=
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+@[grind =] theorem nodup_append {l₁ l₂ : List α} :
+    (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, a ≠ b :=
+  pairwise_append
+
+theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
 grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₁
@@ -312,4 +316,48 @@ theorem getElem?_inj {xs : List α}
 @[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
     (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
 
+theorem Nodup.count [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : Nodup l) : count a l = if a ∈ l then 1 else 0 := by
+  split <;> rename_i h'
+  · obtain ⟨s, t, rfl⟩ := List.append_of_mem h'
+    rw [nodup_append] at h
+    simp_all
+    rw [count_eq_zero.mpr ?_, count_eq_zero.mpr ?_]
+    · exact h.2.1.1
+    · intro w
+      simpa using h.2.2 _ w
+  · rw [count_eq_zero_of_not_mem h']
+
+grind_pattern Nodup.count => count a l, Nodup l
+
+@[grind =]
+theorem nodup_iff_count [BEq α] [LawfulBEq α] {l : List α} : l.Nodup ↔ ∀ a, count a l ≤ 1 := by
+  induction l with
+  | nil => simp
+  | cons x l ih =>
+    constructor
+    · intro h a
+      simp at h
+      rw [count_cons]
+      split <;> rename_i h'
+      · simp at h'
+        rw [count_eq_zero.mpr ?_]
+        · exact Nat.le_refl _
+        · exact h' ▸ h.1
+      · simp at h'
+        refine ih.mp h.2 a
+    · intro h
+      simp only [count_cons] at h
+      simp only [nodup_cons]
+      constructor
+      · intro w
+        specialize h x
+        simp at h
+        have := count_pos_iff.mpr w
+        replace h := le_of_lt_succ h
+        apply Nat.lt_irrefl _ (Nat.lt_of_lt_of_le this h)
+      · rw [ih]
+        intro a
+        specialize h a
+        exact le_of_add_right_le h
+
 end List

src/Init/Data/List/Perm.lean

@@ -23,8 +23,7 @@ The notation `~` is used for permutation equivalence.
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- TODO: restore after an update-stage0
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 
@@ -90,6 +89,9 @@ theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l
   | swap => simp only [mem_cons, or_left_comm]
   | trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]
 
+grind_pattern Perm.mem_iff => l₁ ~ l₂, a ∈ l₁
+grind_pattern Perm.mem_iff => l₁ ~ l₂, a ∈ l₂
+
 theorem Perm.subset {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂ := fun _ => p.mem_iff.mp
 
 theorem Perm.append_right {l₁ l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁ := by
@@ -106,9 +108,15 @@ theorem Perm.append_left {t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂
 theorem Perm.append {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂ :=
   (p₁.append_right t₁).trans (p₂.append_left l₂)
 
+grind_pattern Perm.append => l₁ ~ l₂, t₁ ~ t₂, l₁ ++ t₁
+grind_pattern Perm.append => l₁ ~ l₂, t₁ ~ t₂, l₂ ++ t₂
+
 theorem Perm.append_cons (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : r₁ ~ r₂) :
     l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ := p₁.append (p₂.cons a)
 
+grind_pattern Perm.append_cons => l₁ ~ l₂, r₁ ~ r₂, l₁ ++ a :: r₁
+grind_pattern Perm.append_cons => l₁ ~ l₂, r₁ ~ r₂, l₂ ++ a :: r₂
+
 @[simp] theorem perm_middle {a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
   | [], _ => .refl _
   | b :: _, _ => (Perm.cons _ perm_middle).trans (swap a b _)
@@ -194,9 +202,15 @@ theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~
   | swap x y l₂ => cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap_cons, swap]
   | trans _p₁ _p₂ IH₁ IH₂ => exact IH₁.trans IH₂
 
+grind_pattern Perm.filterMap => l₁ ~ l₂, filterMap f l₁
+grind_pattern Perm.filterMap => l₁ ~ l₂, filterMap f l₂
+
 theorem Perm.map (f : α → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) : map f l₁ ~ map f l₂ :=
   filterMap_eq_map ▸ p.filterMap _
 
+grind_pattern Perm.map => l₁ ~ l₂, map f l₁
+grind_pattern Perm.map => l₁ ~ l₂, map f l₂
+
 theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) {H₁ H₂} :
     pmap f l₁ H₁ ~ pmap f l₂ H₂ := by
   induction p with
@@ -205,12 +219,18 @@ theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α
   | swap x y => simp [swap]
   | trans _p₁ p₂ IH₁ IH₂ => exact IH₁.trans (IH₂ (H₁ := fun a m => H₂ a (p₂.subset m)))
 
+grind_pattern Perm.pmap => l₁ ~ l₂, pmap f l₁ H₁
+grind_pattern Perm.pmap => l₁ ~ l₂, pmap f l₂ H₂
+
 theorem Perm.unattach {α : Type u} {p : α → Prop} {l₁ l₂ : List { x // p x }} (h : l₁ ~ l₂) :
     l₁.unattach.Perm l₂.unattach := h.map _
 
 theorem Perm.filter (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
     filter p l₁ ~ filter p l₂ := by rw [← filterMap_eq_filter]; apply s.filterMap
 
+grind_pattern Perm.filter => l₁ ~ l₂, filter p l₁
+grind_pattern Perm.filter => l₁ ~ l₂, filter p l₂
+
 theorem filter_append_perm (p : α → Bool) (l : List α) :
     filter p l ++ filter (fun x => !p x) l ~ l := by
   induction l with
@@ -388,12 +408,16 @@ theorem Perm.erase (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase
     have h₂ : a ∉ l₂ := mt p.mem_iff.2 h₁
     rw [erase_of_not_mem h₁, erase_of_not_mem h₂]; exact p
 
+grind_pattern Perm.erase => l₁ ~ l₂, l₁.erase a
+grind_pattern Perm.erase => l₁ ~ l₂, l₂.erase a
+
 theorem cons_perm_iff_perm_erase {a : α} {l₁ l₂ : List α} :
     a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a := by
   refine ⟨fun h => ?_, fun ⟨m, h⟩ => (h.cons a).trans (perm_cons_erase m).symm⟩
   have : a ∈ l₂ := h.subset mem_cons_self
   exact ⟨this, (h.trans <| perm_cons_erase this).cons_inv⟩
 
+@[grind =]
 theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂ := by
   refine ⟨Perm.count_eq, fun H => ?_⟩
   induction l₁ generalizing l₂ with
@@ -410,6 +434,12 @@ theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l
     rw [(perm_cons_erase this).count_eq] at H
     by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj] using H
 
+theorem Perm.count (h : l₁ ~ l₂) (a : α) : count a l₁ = count a l₂ := by
+  rw [perm_iff_count.mp h]
+
+grind_pattern Perm.count => l₁ ~ l₂, count a l₁
+grind_pattern Perm.count => l₁ ~ l₂, count a l₂
+
 theorem isPerm_iff : ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
   | [], [] => by simp [isPerm, isEmpty]
   | [], _ :: _ => by simp [isPerm, isEmpty, Perm.nil_eq]
@@ -425,6 +455,9 @@ protected theorem Perm.insert (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
     have := p.cons a
     simpa [h, mt p.mem_iff.2 h] using this
 
+grind_pattern Perm.insert => l₁ ~ l₂, l₁.insert a
+grind_pattern Perm.insert => l₁ ~ l₂, l₂.insert a
+
 theorem perm_insert_swap (x y : α) (l : List α) :
     List.insert x (List.insert y l) ~ List.insert y (List.insert x l) := by
   by_cases xl : x ∈ l <;> by_cases yl : y ∈ l <;> simp [xl, yl]
@@ -491,6 +524,9 @@ theorem Perm.nodup {l l' : List α} (hl : l ~ l') (hR : l.Nodup) : l'.Nodup := h
 theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ → (Nodup l₁ ↔ Nodup l₂) :=
   Perm.pairwise_iff <| @Ne.symm α
 
+grind_pattern Perm.nodup_iff => l₁ ~ l₂, Nodup l₁
+grind_pattern Perm.nodup_iff => l₁ ~ l₂, Nodup l₂
+
 theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten := by
   induction h with
   | nil => rfl
@@ -541,20 +577,30 @@ theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
 
 namespace Perm
 
-theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n ~ l₂.drop n) :
-    l₁.take n ~ l₂.take n := by
+theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : l₁.drop i ~ l₂.drop i) :
+    l₁.take i ~ l₂.take i := by
   classical
   rw [perm_iff_count] at h w ⊢
-  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
+  rw [← take_append_drop i l₁, ← take_append_drop i l₂] at h
   simpa only [count_append, w, Nat.add_right_cancel_iff] using h
 
-theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.take n ~ l₂.take n) :
-    l₁.drop n ~ l₂.drop n := by
+theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : l₁.take i ~ l₂.take i) :
+    l₁.drop i ~ l₂.drop i := by
   classical
   rw [perm_iff_count] at h w ⊢
-  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
+  rw [← take_append_drop i l₁, ← take_append_drop i l₂] at h
   simpa only [count_append, w, Nat.add_left_cancel_iff] using h
 
+theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum := by
+  induction h with
+  | nil => simp
+  | cons _ _ ih => simp [ih]
+  | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
+  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
+
+grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
+grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
+
 end Perm
 
 end List

src/Init/Data/Vector/Count.lean

@@ -40,6 +40,7 @@ theorem countP_push {a : α} {xs : Vector α n} : countP p (xs.push a) = countP
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_push]
 
+@[grind =]
 theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
   simp
 
@@ -51,7 +52,7 @@ theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_le_size (p := p)]
 
-@[simp] theorem countP_append {xs : Vector α n} {ys : Vector α m} : countP p (xs ++ ys) = countP p xs + countP p ys := by
+@[simp, grind =] theorem countP_append {xs : Vector α n} {ys : Vector α m} : countP p (xs ++ ys) = countP p xs + countP p ys := by
   cases xs
   cases ys
   simp
@@ -116,7 +117,7 @@ theorem countP_flatMap {p : β → Bool} {xs : Vector α n} {f : α → Vector
   rcases xs with ⟨xs, rfl⟩
   simp [Array.countP_flatMap, Function.comp_def]
 
-@[simp] theorem countP_reverse {xs : Vector α n} : countP p xs.reverse = countP p xs := by
+@[simp, grind =] theorem countP_reverse {xs : Vector α n} : countP p xs.reverse = countP p xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -136,7 +137,7 @@ section count
 
 variable [BEq α]
 
-@[simp] theorem count_empty {a : α} : count a #v[] = 0 := rfl
+@[simp, grind =] theorem count_empty {a : α} : count a #v[] = 0 := rfl
 
 theorem count_push {a b : α} {xs : Vector α n} :
     count a (xs.push b) = count a xs + if b == a then 1 else 0 := by
@@ -151,23 +152,25 @@ theorem count_eq_countP' {a : α} : count (n := n) a = countP (· == a) := by
 
 theorem count_le_size {a : α} {xs : Vector α n} : count a xs ≤ n := countP_le_size
 
+grind_pattern count_le_size => count a xs
+
 theorem count_le_count_push {a b : α} {xs : Vector α n} : count a xs ≤ count a (xs.push b) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.count_push]
 
-@[simp] theorem count_singleton {a b : α} : count a #v[b] = if b == a then 1 else 0 := by
+@[simp, grind =] theorem count_singleton {a b : α} : count a #v[b] = if b == a then 1 else 0 := by
   simp [count_eq_countP]
 
-@[simp] theorem count_append {a : α} {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind =] theorem count_append {a : α} {xs : Vector α n} {ys : Vector α m} :
     count a (xs ++ ys) = count a xs + count a ys :=
   countP_append ..
 
-@[simp] theorem count_flatten {a : α} {xss : Vector (Vector α m) n} :
+@[simp, grind =] theorem count_flatten {a : α} {xss : Vector (Vector α m) n} :
     count a xss.flatten = (xss.map (count a)).sum := by
   rcases xss with ⟨xss, rfl⟩
   simp [Array.count_flatten, Function.comp_def]
 
-@[simp] theorem count_reverse {a : α} {xs : Vector α n} : count a xs.reverse = count a xs := by
+@[simp, grind =] theorem count_reverse {a : α} {xs : Vector α n} : count a xs.reverse = count a xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 

src/Init/Data/Vector/Range.lean

@@ -120,6 +120,17 @@ theorem range'_eq_append_iff : range' s (n + m) = xs ++ ys ↔ xs = range' s n
     (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i := by
   simp [range'_eq_mk_range']
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [range'_eq_mk_range', count_mk, ← Array.count_range' h]
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [range'_eq_mk_range', count_mk, ← Array.count_range_1']
+
+
 /-! ### range -/
 
 @[simp, grind =] theorem getElem_range {i : Nat} (hi : i < n) : (Vector.range n)[i] = i := by
@@ -171,6 +182,12 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp [range_eq_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [range_eq_range', count_range_1']
+  simp
+
 /-! ### zipIdx -/
 
 @[simp]

tests/lean/run/grind_list2.lean

@@ -93,6 +93,14 @@ theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := by grind
 
 /-! ### mem -/
 
+-- I've gone back and forth on this one. It's an expensive lemma to instantiate merely because we see `a ∈ l`,
+-- so globally it is set up with `grind_pattern length_pos_of_mem => a ∈ l, length l`.
+-- While it's quite useful as simply `grind →` in this "very eary theory", it doesn't  seem essential?
+
+section length_pos_of_mem
+
+attribute [local grind →] length_pos_of_mem
+
 theorem not_mem_nil {a : α} : ¬ a ∈ [] := by grind
 
 theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l := by grind
@@ -196,6 +204,8 @@ theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
     (a :: l).contains b = (b == a || l.contains b) := by grind
 
+end length_pos_of_mem
+
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by grind

tests/lean/run/grind_list_count.lean

@@ -122,9 +122,6 @@ theorem count_nil {a : α} : count a [] = 0 := by grind
 theorem count_cons {a b : α} {l : List α} :
     count a (b :: l) = count a l + if b == a then 1 else 0 := by grind
 
-theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := by grind
-theorem count_eq_countP' {a : α} : count a = countP (· == a) := by grind
-
 theorem count_tail {l : List α} (h : l ≠ []) (a : α) :
       l.tail.count a = l.count a - if l.head h == a then 1 else 0 := by
   induction l with grind

tests/lean/run/grind_list_perm.lean

@@ -0,0 +1,21 @@
+open List
+
+example : [3,1,4,2] ~ [2,4,1,3] := by grind
+
+example (xs ys zs : List Nat) (h₁ : xs ⊆ ys) (h₂ : ys ~ zs) : xs ⊆ zs := by grind
+example (xs ys zs : List Nat) (h₁ : xs <+ ys) (h₂ : ys ~ zs) : xs ⊆ zs := by grind
+example (xs ys zs : List Nat) (h₁ : xs ~ ys) (h₂ : ys ~ zs) : xs ~ zs := by grind
+
+example : List.range 10 ~ (List.range 5 ++ List.range' 5 5).reverse := by grind
+
+variable [BEq α] [LawfulBEq α]
+
+example (xs ys : List (List α)) (h : xs ~ ys) : xs.flatten ~ ys.flatten := by grind
+
+example {l l' : List α} (hl : l ~ l') (_ : l'.Nodup) : l.Nodup := by grind
+
+example {a b : α} {as bs : List α} :
+    a :: as ++ b :: bs ~ b :: as ++ a :: bs := by grind
+
+example (x y : α) (l : List α) :
+    List.insert x (List.insert y l) ~ List.insert y (List.insert x l) := by grind

tests/lean/run/grind_t1.lean

@@ -188,7 +188,6 @@ trace: [grind.assert] ∀ (a : α), a ∈ b → p a
 [grind.assert] w ∈ b
 [grind.assert] ¬p w
 [grind.ematch.instance] h₁: w ∈ b → p w
-[grind.ematch.instance] List.length_pos_of_mem: w ∈ b → 0 < b.length
 [grind.assert] w ∈ b → p w
 -/
 #guard_msgs (trace) in