From bddf6fbf450075bc128d350ff20960b6105b708f Mon Sep 17 00:00:00 2001 From: monsterkrampe Date: Tue, 3 Dec 2024 16:15:57 +0100 Subject: [PATCH] Adjust simp spacing --- src/Std/Data/DHashMap/Internal/Model.lean | 6 +++--- src/Std/Data/DHashMap/Internal/Raw.lean | 4 ++-- src/Std/Data/DHashMap/Internal/WF.lean | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 8b7eb32018a0..713e39efc098 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -480,7 +480,7 @@ theorem insertMany_eq_insertListₘ [BEq α] [Hashable α](m : Raw₀ α β) (l t.val.insertListₘ l from this _ intro t induction l generalizing m with - | nil => simp[insertListₘ] + | nil => simp [insertListₘ] | cons hd tl ih => simp only [List.foldl_cons,insertListₘ] apply ih @@ -524,7 +524,7 @@ theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α Const.insertListₘ t.val l from this _ intro t induction l generalizing m with - | nil => simp[insertListₘ] + | nil => simp [insertListₘ] | cons hd tl ih => simp only [List.foldl_cons,insertListₘ] apply ih @@ -538,7 +538,7 @@ theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ [BEq α] [Hashable Const.insertListIfNewUnitₘ t.val l from this _ intro t induction l generalizing m with - | nil => simp[insertListIfNewUnitₘ] + | nil => simp [insertListIfNewUnitₘ] | cons hd tl ih => simp only [List.foldl_cons,insertListIfNewUnitₘ] apply ih diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index 4fcbb00d42a2..a735d30d7dd3 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -201,11 +201,11 @@ theorem filter_val [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → theorem insertMany_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} : m.insertMany l = Raw₀.insertMany ⟨m, h.size_buckets_pos⟩ l := by - simp[Raw.insertMany, h.size_buckets_pos] + simp [Raw.insertMany, h.size_buckets_pos] theorem insertMany_val [BEq α][Hashable α] {m : Raw₀ α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} : m.val.insertMany l = m.insertMany l := by - simp[Raw.insertMany, m.2] + simp [Raw.insertMany, m.2] section diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 97b135282e0e..7c199d9a3a09 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -723,7 +723,7 @@ theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHas Perm (toListModel (insertListₘ m l).1.buckets) (List.insertList (toListModel m.1.buckets) l) := by induction l generalizing m with | nil => - simp[insertListₘ, List.insertList] + simp [insertListₘ, List.insertList] | cons hd tl ih => simp only [insertListₘ, List.insertList] apply Perm.trans