[Merged by Bors] - feat: grind golf in Mathlib.Data.List

Mathlib/Data/List/Basic.lean

@@ -157,15 +157,10 @@ theorem exists_mem_cons_of_exists {p : α → Prop} {a : α} {l : List α} : (
   fun ⟨x, xl, px⟩ => ⟨x, mem_cons_of_mem _ xl, px⟩
 
 theorem or_exists_of_exists_mem_cons {p : α → Prop} {a : α} {l : List α} : (∃ x ∈ a :: l, p x) →
-    p a ∨ ∃ x ∈ l, p x :=
-  fun ⟨x, xal, px⟩ =>
-    Or.elim (eq_or_mem_of_mem_cons xal) (fun h : x = a => by rw [← h]; left; exact px)
-      fun h : x ∈ l => Or.inr ⟨x, h, px⟩
+    p a ∨ ∃ x ∈ l, p x := by grind
 
 theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : List α) :
-    (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x :=
-  Iff.intro or_exists_of_exists_mem_cons fun h =>
-    Or.elim h (exists_mem_cons_of l) exists_mem_cons_of_exists
+    (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x := by grind
 
 /-! ### list subset -/
 
@@ -303,9 +298,7 @@ theorem getLast_append_singleton {a : α} (l : List α) :
 
 theorem getLast_append_of_right_ne_nil (l₁ l₂ : List α) (h : l₂ ≠ []) :
     getLast (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = getLast l₂ h := by
-  induction l₁ with
-  | nil => simp
-  | cons _ _ ih => simp only [cons_append]; rw [List.getLast_cons]; exact ih
+  induction l₁ with grind
 
 theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (by simp) = a := by
   simp
@@ -332,15 +325,9 @@ theorem getLast_replicate_succ (m : ℕ) (a : α) :
 /-! ### getLast? -/
 
 theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? → ∃ h, x = getLast l h
-  | [], x, hx => False.elim <| by simp at hx
-  | [a], x, hx =>
-    have : a = x := by simpa using hx
-    this ▸ ⟨cons_ne_nil a [], rfl⟩
-  | a :: b :: l, x, hx => by
-    rw [getLast?_cons_cons] at hx
-    rcases mem_getLast?_eq_getLast hx with ⟨_, h₂⟩
-    use cons_ne_nil _ _
-    assumption
+  | [], x, hx
+  | [a], x, hx
+  | a :: b :: l, x, hx => by grind
 
 theorem getLast?_eq_getLast_of_ne_nil : ∀ {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
   | [], h => (h rfl).elim
@@ -378,11 +365,7 @@ theorem getLast?_append_of_ne_nil (l₁ : List α) :
   | b :: l₂, _ => getLast?_append_cons l₁ b l₂
 
 theorem mem_getLast?_append_of_mem_getLast? {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) :
-    x ∈ (l₁ ++ l₂).getLast? := by
-  cases l₂
-  · contradiction
-  · rw [List.getLast?_append_cons]
-    exact h
+    x ∈ (l₁ ++ l₂).getLast? := by grind
 
 /-! ### head(!?) and tail -/
 
@@ -433,10 +416,7 @@ theorem head?_append_of_ne_nil :
   | _ :: _, _, _ => rfl
 
 theorem tail_append_singleton_of_ne_nil {a : α} {l : List α} (h : l ≠ nil) :
-    tail (l ++ [a]) = tail l ++ [a] := by
-  induction l
-  · contradiction
-  · rw [tail, cons_append, tail]
+    tail (l ++ [a]) = tail l ++ [a] := by grind
 
 theorem cons_head?_tail : ∀ {l : List α} {a : α}, a ∈ head? l → a :: tail l = l
   | [], a, h => by contradiction
@@ -518,12 +498,10 @@ theorem idxOf_of_notMem {l : List α} {a : α} : a ∉ l → idxOf a l = length
 
 @[deprecated (since := "2025-05-23")] alias idxOf_of_not_mem := idxOf_of_notMem
 
-theorem idxOf_append_of_mem {a : α} (h : a ∈ l₁) : idxOf a (l₁ ++ l₂) = idxOf a l₁ := by
-  grind
+theorem idxOf_append_of_mem {a : α} (h : a ∈ l₁) : idxOf a (l₁ ++ l₂) = idxOf a l₁ := by grind
 
 theorem idxOf_append_of_notMem {a : α} (h : a ∉ l₁) :
-    idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂ := by
-  grind
+    idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂ := by grind
 
 @[deprecated (since := "2025-05-23")] alias idxOf_append_of_not_mem := idxOf_append_of_notMem
 
@@ -551,10 +529,7 @@ theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length)
 theorem ext_getElem?' {l₁ l₂ : List α} (h' : ∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]?) :
     l₁ = l₂ := by
   apply ext_getElem?
-  intro n
-  rcases Nat.lt_or_ge n <| max l₁.length l₂.length with hn | hn
-  · exact h' n hn
-  · simp_all [Nat.max_le]
+  grind
 
 theorem ext_get_iff {l₁ l₂ : List α} :
     l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩ := by
@@ -604,11 +579,8 @@ theorem get_reverse' (l : List α) (n) (hn') :
     l.reverse.get n = l.get ⟨l.length - 1 - n, hn'⟩ := by
   simp
 
-theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) : l = [l.get ⟨0, by cutsat⟩] := by
-  refine ext_get (by convert h) fun n h₁ h₂ => ?_
-  simp
-  congr
-  cutsat
+theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) : l = [l.get ⟨0, by omega⟩] := by
+  refine ext_get (by convert h) (by grind)
 
 end deprecated
 
@@ -987,18 +959,7 @@ variable (p)
 
 theorem monotone_filter_right (l : List α) ⦃p q : α → Bool⦄
     (h : ∀ a, p a → q a) : l.filter p <+ l.filter q := by
-  induction l with
-  | nil => rfl
-  | cons hd tl IH =>
-    by_cases hp : p hd
-    · rw [filter_cons_of_pos hp, filter_cons_of_pos (h _ hp)]
-      exact IH.cons_cons hd
-    · rw [filter_cons_of_neg hp]
-      by_cases hq : q hd
-      · rw [filter_cons_of_pos hq]
-        exact sublist_cons_of_sublist hd IH
-      · rw [filter_cons_of_neg hq]
-        exact IH
+  induction l with grind
 
 lemma map_filter {f : α → β} (hf : Injective f) (l : List α)
     [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
@@ -1040,8 +1001,7 @@ variable {p : α → Bool}
 
 -- Cannot be @[simp] because `a` cannot be inferred by `simp`.
 theorem length_eraseP_add_one {l : List α} {a} (al : a ∈ l) (pa : p a) :
-    (l.eraseP p).length + 1 = l.length := by
-  grind
+    (l.eraseP p).length + 1 = l.length := by grind
 
 end eraseP
 
@@ -1069,19 +1029,10 @@ theorem erase_getElem [DecidableEq ι] {l : List ι} {i : ℕ} (hi : i < l.lengt
     Perm (l.erase l[i]) (l.eraseIdx i) := by
   induction l generalizing i with
   | nil => simp
-  | cons a l IH =>
-    cases i with
-    | zero => simp
-    | succ i =>
-      have hi' : i < l.length := by simpa using hi
-      if ha : a = l[i] then
-        simpa [ha] using .trans (perm_cons_erase (getElem_mem _)) (.cons _ (IH hi'))
-      else
-        simpa [ha] using IH hi'
+  | cons a l IH => cases i with grind
 
 theorem length_eraseIdx_add_one {l : List ι} {i : ℕ} (h : i < l.length) :
-    (l.eraseIdx i).length + 1 = l.length := by
-  grind
+    (l.eraseIdx i).length + 1 = l.length := by grind
 
 end Erase
 
@@ -1210,12 +1161,7 @@ variable [BEq α] [LawfulBEq α]
 
 lemma lookup_graph (f : α → β) {a : α} {as : List α} (h : a ∈ as) :
     lookup a (as.map fun x => (x, f x)) = some (f a) := by
-  induction as with
-  | nil => exact (not_mem_nil h).elim
-  | cons a' as ih =>
-    by_cases ha : a = a'
-    · simp [ha]
-    · simpa [lookup_cons, beq_false_of_ne ha] using ih (List.mem_of_ne_of_mem ha h)
+  induction as with grind
 
 end lookup
 

Mathlib/Data/List/Flatten.lean

@@ -23,12 +23,7 @@ namespace List
 @[gcongr]
 protected theorem Sublist.flatten {l₁ l₂ : List (List α)} (h : l₁ <+ l₂) :
     l₁.flatten <+ l₂.flatten := by
-  induction h with
-  | slnil => simp
-  | cons _ _ ih =>
-    rw [flatten_cons]
-    exact ih.trans (sublist_append_right _ _)
-  | cons₂ _ _ ih => simpa
+  induction h with grind
 
 @[gcongr]
 protected theorem Sublist.flatMap {l₁ l₂ : List α} (h : l₁ <+ l₂) (f : α → List β) :
@@ -39,20 +34,12 @@ protected theorem Sublist.flatMap {l₁ l₂ : List α} (h : l₁ <+ l₂) (f :
 left with a list of length `1` made of the `i`-th element of the original list. -/
 theorem drop_take_succ_eq_cons_getElem (L : List α) (i : Nat) (h : i < L.length) :
     (L.take (i + 1)).drop i = [L[i]] := by
-  induction L generalizing i with
-  | nil => exact (Nat.not_succ_le_zero i h).elim
-  | cons head tail ih =>
-    rcases i with _ | i
-    · simp
-    · simpa using ih _ (by simpa using h)
+  induction L generalizing i with grind
 
 /-- We can rebracket `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)` to
 `(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` where `L = [l₁, l₂, ..., lₙ]`. -/
 theorem append_flatten_map_append (L : List (List α)) (x : List α) :
     x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x := by
-  induction L with
-  | nil => rw [map_nil, flatten, append_nil, map_nil, flatten, nil_append]
-  | cons _ _ ih =>
-    rw [map_cons, flatten, map_cons, flatten, append_assoc, ih, append_assoc, append_assoc]
+  induction L with grind
 
 end List

Mathlib/Data/List/Induction.lean

@@ -47,14 +47,7 @@ theorem reverseRecOn_concat {motive : List α → Sort*} (x : α) (xs : List α)
     exact this _ (reverse_reverse xs)
   intro ys hy
   conv_lhs => unfold reverseRecOn
-  split
-  next h => simp at h
-  next heq =>
-    revert heq
-    simp only [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, cons.injEq]
-    rintro ⟨rfl, rfl⟩
-    subst ys
-    rfl
+  grind
 
 /-- Bidirectional induction principle for lists: if a property holds for the empty list, the
 singleton list, and `a :: (l ++ [b])` from `l`, then it holds for all lists. This can be used to
@@ -95,20 +88,7 @@ theorem bidirectionalRec_cons_append {motive : List α → Sort*}
     bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
       cons_append a l b (bidirectionalRec nil singleton cons_append l) := by
   conv_lhs => unfold bidirectionalRec
-  cases l with
-  | nil => rfl
-  | cons x xs =>
-  simp only [List.cons_append]
-  dsimp only [← List.cons_append]
-  suffices ∀ (ys init : List α) (hinit : init = ys) (last : α) (hlast : last = b),
-      (cons_append a init last
-        (bidirectionalRec nil singleton cons_append init)) =
-      cast (congr_arg motive <| by simp [hinit, hlast])
-        (cons_append a ys b (bidirectionalRec nil singleton cons_append ys)) by
-    rw [this (x :: xs) _ (by rw [dropLast_append_cons, dropLast_singleton, append_nil]) _ (by simp)]
-    simp
-  rintro ys init rfl last rfl
-  rfl
+  cases l with grind
 
 /-- Like `bidirectionalRec`, but with the list parameter placed first. -/
 @[elab_as_elim]

Mathlib/Data/List/Lattice.lean

@@ -95,7 +95,7 @@ end Union
 
 section Inter
 
-@[simp]
+@[simp, grind =]
 theorem inter_nil (l : List α) : [] ∩ l = [] :=
   rfl
 
@@ -107,13 +107,16 @@ theorem inter_cons_of_mem (l₁ : List α) (h : a ∈ l₂) : (a :: l₁) ∩ l
 theorem inter_cons_of_notMem (l₁ : List α) (h : a ∉ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂ := by
   simp [Inter.inter, List.inter, h]
 
+@[grind =]
+theorem inter_cons (l₁ : List α) :
+    (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂ := by
+  split_ifs <;> simp_all
+
 @[deprecated (since := "2025-05-23")] alias inter_cons_of_not_mem := inter_cons_of_notMem
 
-@[simp]
+@[simp, grind =]
 theorem inter_nil' (l : List α) : l ∩ [] = [] := by
-  induction l with
-  | nil => rfl
-  | cons x xs ih => by_cases x ∈ xs <;> simp [ih]
+  induction l with grind
 
 theorem mem_of_mem_inter_left : a ∈ l₁ ∩ l₂ → a ∈ l₁ :=
   mem_of_mem_filter
@@ -159,68 +162,38 @@ end Inter
 
 section BagInter
 
-@[simp]
+@[simp, grind =]
 theorem nil_bagInter (l : List α) : [].bagInter l = [] := by cases l <;> rfl
 
-@[simp]
+@[simp, grind =]
 theorem bagInter_nil (l : List α) : l.bagInter [] = [] := by cases l <;> rfl
 
 @[simp]
 theorem cons_bagInter_of_pos (l₁ : List α) (h : a ∈ l₂) :
     (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a) := by
-  cases l₂
-  · exact if_pos h
-  · simp only [List.bagInter, if_pos (elem_eq_true_of_mem h)]
+  cases l₂ with grind [List.bagInter]
 
 @[simp]
 theorem cons_bagInter_of_neg (l₁ : List α) (h : a ∉ l₂) :
     (a :: l₁).bagInter l₂ = l₁.bagInter l₂ := by
-  cases l₂; · simp only [bagInter_nil]
-  simp only [erase_of_not_mem h, List.bagInter, if_neg (mt mem_of_elem_eq_true h)]
+  cases l₂ with grind [List.bagInter]
+
+@[grind =]
+theorem cons_bagInteger :
+    (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂ := by
+  split_ifs <;> simp_all
 
 @[simp]
-theorem mem_bagInter {a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
-  | [], l₂ => by simp only [nil_bagInter, not_mem_nil, false_and]
-  | b :: l₁, l₂ => by
-    by_cases h : b ∈ l₂
-    · rw [cons_bagInter_of_pos _ h, mem_cons, mem_cons, mem_bagInter]
-      by_cases ba : a = b
-      · simp only [ba, h, true_or, true_and]
-      · simp only [mem_erase_of_ne ba, ba, false_or]
-    · rw [cons_bagInter_of_neg _ h, mem_bagInter, mem_cons, or_and_right]
-      symm
-      apply or_iff_right_of_imp
-      rintro ⟨rfl, h'⟩
-      exact h.elim h'
+theorem mem_bagInter {a : α} {l₁ l₂ : List α} : a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂ := by
+  fun_induction List.bagInter with grind
 
 @[simp]
-theorem count_bagInter {a : α} :
-    ∀ {l₁ l₂ : List α}, count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
-  | [], l₂ => by simp
-  | l₁, [] => by simp
-  | b :: l₁, l₂ => by
-    by_cases hb : b ∈ l₂
-    · rw [cons_bagInter_of_pos _ hb, count_cons, count_cons, count_bagInter, count_erase,
-        ← Nat.add_min_add_right]
-      by_cases ba : b = a
-      · simp only [beq_iff_eq]
-        rw [if_pos ba, Nat.sub_add_cancel]
-        rwa [succ_le_iff, count_pos_iff, ← ba]
-      · simp only [beq_iff_eq]
-        rw [if_neg ba, Nat.sub_zero, Nat.add_zero, Nat.add_zero]
-    · rw [cons_bagInter_of_neg _ hb, count_bagInter]
-      by_cases ab : a = b
-      · rw [← ab] at hb
-        rw [count_eq_zero.2 hb, Nat.min_zero, Nat.min_zero]
-      · rw [count_cons_of_ne (Ne.symm ab)]
-
-theorem bagInter_sublist_left : ∀ l₁ l₂ : List α, l₁.bagInter l₂ <+ l₁
-  | [], l₂ => by simp
-  | b :: l₁, l₂ => by
-    by_cases h : b ∈ l₂ <;> simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
-    · exact (bagInter_sublist_left _ _).cons_cons _
-    · apply sublist_cons_of_sublist
-      apply bagInter_sublist_left
+theorem count_bagInter {a : α} {l₁ l₂ : List α} :
+    count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂) := by
+  fun_induction List.bagInter with grind [count_pos_iff]
+
+theorem bagInter_sublist_left {l₁ l₂ : List α} : l₁.bagInter l₂ <+ l₁ := by
+  fun_induction List.bagInter with grind
 
 theorem bagInter_nil_iff_inter_nil : ∀ l₁ l₂ : List α, l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
   | [], l₂ => by simp