From fd142a57dc49480ae1fcb6affa6cdccaf8f44c88 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Fri, 6 Feb 2026 01:09:52 +0000
Subject: [PATCH 1/2] chore: golf proofs about merge

---
 .../Algorithms/Lean/MergeSort/MergeSort.lean  | 26 +++++++++----------
 1 file changed, 12 insertions(+), 14 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 31f05103..9316142d 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -63,6 +63,14 @@ section Correctness
 
 open List
 
+/-- Our merge computes the one already in mathlib. -/
+@[simp, grind =]
+theorem ret_merge (xs ys : List α) : ⟪merge xs ys⟫ = xs.merge ys := by
+  fun_induction merge
+  · simp
+  · simp
+  · grind [cons_merge_cons]
+
 /-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/
 abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l
 
@@ -71,11 +79,7 @@ abbrev MinOfList (x : α) (l : List α) : Prop := ∀ b ∈ l, x ≤ b
 
 @[grind →]
 theorem mem_either_merge (xs ys : List α) (z : α) (hz : z ∈ ⟪merge xs ys⟫) : z ∈ xs ∨ z ∈ ys := by
-  fun_induction merge
-  · exact mem_reverseAux.mp hz
-  · left
-    exact hz
-  · grind
+  grind [List.mem_merge]
 
 theorem min_all_merge (x : α) (xs ys : List α) (hxs : MinOfList x xs) (hys : MinOfList x ys) :
     MinOfList x ⟪merge xs ys⟫ := by
@@ -83,10 +87,7 @@ theorem min_all_merge (x : α) (xs ys : List α) (hxs : MinOfList x xs) (hys : M
 
 theorem sorted_merge {l1 l2 : List α} (hxs : IsSorted l1) (hys : IsSorted l2) :
     IsSorted ⟪merge l1 l2⟫ := by
-  fun_induction merge l1 l2 with
-  | case3 =>
-    grind [pairwise_cons]
-  | _ => simpa
+  grind [hxs.merge hys]
 
 theorem mergeSort_sorted (xs : List α) : IsSorted ⟪mergeSort xs⟫ := by
   fun_induction mergeSort xs with
@@ -177,16 +178,13 @@ theorem timeMergeSortRec_le (n : ℕ) : timeMergeSortRec n ≤ T n := by
 
 @[simp] theorem merge_ret_length_eq_sum (xs ys : List α) :
     ⟪merge xs ys⟫.length = xs.length + ys.length := by
-  fun_induction merge with
-  | case3 =>
-    grind
-  | _ => simp
+  simp
 
 @[simp] theorem mergeSort_same_length (xs : List α) :
     ⟪mergeSort xs⟫.length = xs.length := by
   fun_induction mergeSort
   · simp
-  · grind [merge_ret_length_eq_sum]
+  · grind [List.length_merge]
 
 @[simp] theorem merge_time (xs ys : List α) : (merge xs ys).time ≤ xs.length + ys.length := by
   fun_induction merge with

From 2de969b0c3243195086fd846bac4df419eeeeef4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Tue, 24 Feb 2026 17:56:13 +0000
Subject: [PATCH 2/2] fixes

---
 Cslib/Algorithms/Lean/MergeSort/MergeSort.lean | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 9316142d..8ba55d46 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -66,10 +66,7 @@ open List
 /-- Our merge computes the one already in mathlib. -/
 @[simp, grind =]
 theorem ret_merge (xs ys : List α) : ⟪merge xs ys⟫ = xs.merge ys := by
-  fun_induction merge
-  · simp
-  · simp
-  · grind [cons_merge_cons]
+  fun_induction merge with grind [nil_merge, merge_right, cons_merge_cons]
 
 /-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/
 abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l
@@ -96,11 +93,7 @@ theorem mergeSort_sorted (xs : List α) : IsSorted ⟪mergeSort xs⟫ := by
   | case2 _ _ _ _ _ ih2 ih1 => exact sorted_merge ih2 ih1
 
 lemma merge_perm (l₁ l₂ : List α) : ⟪merge l₁ l₂⟫ ~ l₁ ++ l₂ := by
-  fun_induction merge with
-  | case1 => simp
-  | case2 => simp
-  | case3 =>
-    grind
+  fun_induction merge with grind [List.merge_perm_append]
 
 theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by
   fun_induction mergeSort xs with
@@ -136,8 +129,7 @@ open Nat (clog)
 /-- Key Lemma: ⌈log2 ⌈n/2⌉⌉ ≤ ⌈log2 n⌉ - 1 for n > 1 -/
 @[grind →]
 lemma clog2_half_le (n : ℕ) (h : n > 1) : clog 2 ((n + 1) / 2) ≤ clog 2 n - 1 := by
-  rw [Nat.clog_of_one_lt one_lt_two h]
-  grind
+  grind [Nat.clog_of_one_lt one_lt_two h]
 
 /-- Same logic for the floor half: ⌈log2 ⌊n/2⌋⌉ ≤ ⌈log2 n⌉ - 1 -/
 @[grind →]
@@ -176,7 +168,7 @@ theorem timeMergeSortRec_le (n : ℕ) : timeMergeSortRec n ≤ T n := by
     have := some_algebra n
     grind [Nat.add_div_right]
 
-@[simp] theorem merge_ret_length_eq_sum (xs ys : List α) :
+theorem merge_ret_length_eq_sum (xs ys : List α) :
     ⟪merge xs ys⟫.length = xs.length + ys.length := by
   simp