From 21d71de481e3d497a3ceeac85e50b50338b5636d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 17 Sep 2024 22:43:39 +1000 Subject: [PATCH] chore: fix name of List.length_mergeSort (#5373) --- src/Init/Data/List/Sort/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index bf35c2d61afc..686113748fc0 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -234,7 +234,7 @@ theorem mergeSort_perm : ∀ (l : List α) (le), mergeSort l le ~ l (Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _))) termination_by l => l.length -@[simp] theorem mergeSort_length (l : List α) : (mergeSort l le).length = l.length := +@[simp] theorem length_mergeSort (l : List α) : (mergeSort l le).length = l.length := (mergeSort_perm l le).length_eq @[simp] theorem mem_mergeSort {a : α} {l : List α} : a ∈ mergeSort l le ↔ a ∈ l :=