From 41bb40b762bf2665779c020ceb45f4b7430baa4b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 10 Sep 2024 18:45:31 +1000
Subject: [PATCH] long lines

---
 Batteries/Data/Array/Lemmas.lean   | 9 ++++++---
 Batteries/Data/Array/Pairwise.lean | 3 ++-
 Batteries/Data/HashMap/WF.lean     | 8 ++++----
 Batteries/Data/List/Basic.lean     | 5 +++--
 4 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 35139ddce0..ee12d886e9 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -36,7 +36,8 @@ theorem forIn_eq_forIn_toList [Monad m]
 theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
     (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
   let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
-      (zipWithAux f as bs i cs).toList = cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
+      (zipWithAux f as bs i cs).toList =
+        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
     intro i cs hia hib
     unfold zipWithAux
     by_cases h : i = as.size ∨ i = bs.size
@@ -67,7 +68,8 @@ theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
       let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
       rw [h₁, List.append_assoc]
       congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_toList_getElem, getElem_eq_toList_getElem]
+      rw [← List.zipWith_append (h := by simp), getElem_eq_toList_getElem,
+        getElem_eq_toList_getElem]
       show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
         ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
         List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
@@ -122,7 +124,8 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L 
 
 /-! ### erase -/
 
-@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} : (l.erase a).toList = l.toList.erase a
+@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
+    (l.erase a).toList = l.toList.erase a
 
 /-! ### shrink -/
 
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index b4151c5a0a..1a71924c1c 100644
--- a/Batteries/Data/Array/Pairwise.lean
+++ b/Batteries/Data/Array/Pairwise.lean
@@ -51,7 +51,8 @@ theorem pairwise_append {as bs : Array α} :
 theorem pairwise_push {as : Array α} :
     (as.push a).Pairwise R ↔ as.Pairwise R ∧ (∀ x ∈ as, R x a) := by
   unfold Pairwise
-  simp [← mem_toList, push_toList, List.pairwise_append, List.pairwise_singleton, List.mem_singleton]
+  simp [← mem_toList, push_toList, List.pairwise_append, List.pairwise_singleton,
+    List.mem_singleton]
 
 theorem pairwise_extract {as : Array α} (h : as.Pairwise R) (start stop) :
     (as.extract start stop).Pairwise R := by
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index 2bb7d09cde..993e9e10d4 100644
--- a/Batteries/Data/HashMap/WF.lean
+++ b/Batteries/Data/HashMap/WF.lean
@@ -60,8 +60,8 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H :
     | .inl hl => H.1 _ hl
     | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..))
   · revert hp
-    simp only [Array.getElem_eq_toList_getElem, toList_update, List.getElem_set, Array.toList_length,
-      update_size]
+    simp only [Array.getElem_eq_toList_getElem, toList_update, List.getElem_set,
+      Array.toList_length, update_size]
     split <;> intro hp
     · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp
     · simp only [update_size, Array.toList_length] at hi
@@ -171,8 +171,8 @@ where
       · match List.mem_or_eq_of_mem_set hl with
         | .inl hl => exact hs₁ _ hl
         | .inr e => exact e ▸ .nil
-      · simp only [Array.toList_length, Array.size_set, Array.getElem_eq_toList_getElem, Array.toList_set,
-          List.getElem_set]
+      · simp only [Array.toList_length, Array.size_set, Array.getElem_eq_toList_getElem,
+          Array.toList_set, List.getElem_set]
         split
         · nofun
         · exact hs₂ _ (by simp_all)
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 1ac57bb04a..405f2a4ea9 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -149,8 +149,9 @@ def splitOnP (P : α → Bool) (l : List α) : List (List α) := go l [] where
 
 @[csimp] theorem splitOnP_eq_splitOnPTR : @splitOnP = @splitOnPTR := by
   funext α P l; simp [splitOnPTR]
-  suffices ∀ xs acc r, splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse from
-    (this l #[] #[]).symm
+  suffices ∀ xs acc r,
+    splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse from
+      (this l #[] #[]).symm
   intro xs acc r; induction xs generalizing acc r with simp [splitOnP.go, splitOnPTR.go]
   | cons x xs IH => cases P x <;> simp [*]