chore(Data/List/SplitBy): golf theorems (#30896)

Author: vihdzp

Mathlib/Data/List/SplitBy.lean

@@ -11,7 +11,7 @@ import Mathlib.Data.List.Chain
 This file provides the basic API for `List.splitBy` which is defined in Core.
 The main results are the following:
 
-- `List.join_splitBy`: the lists in `List.splitBy` join to the original list.
+- `List.flatten_splitBy`: the lists in `List.splitBy` join to the original list.
 - `List.nil_notMem_splitBy`: the empty list is not contained in `List.splitBy`.
 - `List.isChain_of_mem_splitBy`: any two adjacent elements in a list in
   `List.splitBy` are related by the specified relation.
@@ -54,8 +54,7 @@ theorem flatten_splitBy (r : α → α → Bool) (l : List α) : (l.splitBy r).f
 private theorem nil_notMem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} :
     [] ∉ splitBy.loop r l a g [] := by
   induction l generalizing a g with
-  | nil =>
-    simp [splitBy.loop]
+  | nil => simp [splitBy.loop]
   | cons b l IH =>
     rw [splitBy.loop]
     split
@@ -65,16 +64,16 @@ private theorem nil_notMem_splitByLoop {r : α → α → Bool} {l : List α} {a
 
 @[deprecated (since := "2025-05-23")] alias nil_not_mem_splitByLoop := nil_notMem_splitByLoop
 
+@[simp]
 theorem nil_notMem_splitBy (r : α → α → Bool) (l : List α) : [] ∉ l.splitBy r :=
   match l with
   | nil => not_mem_nil
   | cons _ _ => nil_notMem_splitByLoop
 
 @[deprecated (since := "2025-05-23")] alias nil_not_mem_splitBy := nil_notMem_splitBy
 
-theorem ne_nil_of_mem_splitBy (r : α → α → Bool) {l : List α} (h : m ∈ l.splitBy r) : m ≠ [] := by
-  rintro rfl
-  exact nil_notMem_splitBy r l h
+theorem ne_nil_of_mem_splitBy {r : α → α → Bool} {l : List α} (h : m ∈ l.splitBy r) : m ≠ [] :=
+  fun _ ↦ by simp_all
 
 private theorem isChain_of_mem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α}
     (hga : ∀ b ∈ g.head?, r b a) (hg : g.IsChain fun y x ↦ r x y)
@@ -83,33 +82,26 @@ private theorem isChain_of_mem_splitByLoop {r : α → α → Bool} {l : List α
   | nil =>
     rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
     obtain hm | rfl := h
-    · exact (not_mem_nil hm).elim
+    · cases not_mem_nil hm
     · apply List.isChain_reverse.1
       rw [reverse_reverse]
       exact isChain_cons.2 ⟨hga, hg⟩
   | cons b l IH =>
     simp only [splitBy.loop, reverse_cons] at h
     split at h
     · apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
-      intro b hb
-      rw [head?_cons, Option.mem_some_iff] at hb
-      rwa [← hb]
+      grind
     · rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
       obtain rfl | hm := h
       · apply List.isChain_reverse.1
         rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
         exact isChain_cons.2 ⟨hga, hg⟩
-      · apply IH _ isChain_nil hm
-        rintro _ ⟨⟩
+      · grind
 
 theorem isChain_of_mem_splitBy {r : α → α → Bool} {l : List α} (h : m ∈ l.splitBy r) :
     m.IsChain fun x y ↦ r x y := by
-  cases l with
-  | nil => cases h
-  | cons a l =>
-    apply isChain_of_mem_splitByLoop _ _ h
-    · rintro _ ⟨⟩
-    · exact isChain_nil
+  match l, h with
+  | a::l, h => apply isChain_of_mem_splitByLoop _ _ h <;> simp
 
 @[deprecated (since := "2025-09-24")] alias chain'_of_mem_splitBy := isChain_of_mem_splitBy